本位田真一のレビュー一覧

SPINによる設計モデル検証

本位田真一 / 萩谷昌己 / 吉岡信和 / 青木利晃 / 田原康之

形式手法の教育を行う場合に、受講生は全部読んでいる必要はないという命題をたててみました。

というのは、トップエスイー実践講座３では、「高度な数学的知識を習得して、現実的なシステムの仕様記述に利用することは容易でははい。」「モデル検査は、検証に必要な証明の作業を完全に自動的に行うため、上述の形式検証技術一般の問題点を解決できる。」とあることにもとづいています。

ただし、講師になる人間は、全部読んでいる必要があると感じました。

本書を読む前に、「四日で学ぶモデル検証」を実際に動かした方がよいと感じています。
自分では、本書も先に目を通そうとしたことがありましたが、めげていました。

「四日で学ぶモデル検証」をやってからは、少なくとも動作させたことがある部分は、
読み進むことができました。

ソフトウェア科学基礎

本位田真一 / 田中譲 / 磯部祥尚 / 粂野文洋 / 櫻庭健年 / 田口研治

形式手法の教育を行う場合に、受講生は、本書を全部読んでいる必要はないという命題をたててみました。

トップエスイー実践講座３では、「高度な数学的知識を習得して、現実的なシステムの仕様記述に利用することは容易でははい。」「モデル検査は、検証に必要な証明の作業を完全に自動的に行うため、上述の形式検証技術一般の問題点を解決できる。」とあることにもとづいています。

講師になる人間は、全部読んでいる必要があると感じました。
本書を読んでいて、わからない記述があったので記録します。

P21
論理命題が真であれば、その対偶は真となる。

「叱らないと勉強しない」（命題）
「勉強すると叱る」（対偶）

解釈としては
「勉強しているということは叱られたから」
という記述がありました。

疑問に思った点は、勉強していはじめたときと、叱ったときが同時でればよいのではないでしょうか。

「勉強しはじめたときにちょうど叱った」
というのが真であれば、
叱る方は「叱らないと勉強しない」と思うし、
勉強している方は、「勉強しはじめたときにちょうど叱った」と思うという理解ではだめでしょうか。

そのため、対偶としては、
「勉強しはじめたときにちょうど叱った」
といのではだめでしょうか。

あるいは、
叱る側の立場
「叱らないと勉強しない」
「勉強しているということは叱られたから」
というのは、すでに順序関係を含んでいるので、その記載がないことが問題なのでしょうか。

ところで、勉強する側の立場
「勉強しはじめたときにちょうど叱った」
の対偶は
「叱らなかったときに、勉強を始めなかったことがある」
というのでよいでしょうか？

ps.
命題が複数の人間に関するものは、表現を注意する必要があるのではという理解でよいでしょうか。

Bメソッドによる形式仕様記述

本位田真一 / 中島震 / 来間啓伸

抽象機械、変数の宣言、不変条件の宣言、変数の初期化、操作の定義、一般化代入の紹介がある。
抽象機械の整合性の検証として、最弱事前条件、不変条件の無矛盾性、初期化の整合性について説明がある。
集合論的に厳密に記述していくのがミソのようです。
Refinementという段階的詳細化をしていって実装までたどり着きます。各段階間の整合性を確認することによって、実装が抽象的に検討した性格を保っていることを保証します。
トップエスイー講座は受けにいけませんでした。

読者である北海道立工業試験場の堀さんに２度講習会を開いていただきました。

アジャイルイントロダクション Agile開発の光と影

本位田真一 / 石川冬樹 / メイヤーバートランド / 土肥拓生 / 前澤悠太 / 末永俊一郎

アジャイル開発にまつわる書籍を広く分析し、長所と短所が客観的に整理されている。確かにアジャイル系の書籍は事例を挙げて一般的に適用可能だと連想させる逸話が多い。
惜しいのはこれが入門書として扱われていること。アジャイル開発を実際に経験し、独自の道に進もうとしている人にこそ読んで欲しい。