ソフトウェア科学基礎: 最先端のソフトウェア開発に求められる数理的基礎 (トップエスイー基礎講座 1)

著者 : 磯部祥尚

• 近代科学社 (2008年9月1日発売)

感想・レビュー・書評

[北海道大学工学研究院中央図書室さんの感想 · 2020年3月16日]

【電子ブックへのリンク先】
https://kinoden.kinokuniya.co.jp/hokudai/bookdetail/p/KP00012219
※学外から利用する場合は、以下のアドレスからご覧ください。（要ログイン）
https://www.lib.hokudai.ac.jp/remote-access/?url=https://kinoden.kinokuniya.co.jp/hokudai/bookdetail/p/KP00012219

[mikumotousanさんの感想 · 2015年12月18日]

形式検証による平行システムの検証を取り上げている
モデル検証の複雑さを軽減する方法も触れている。
機能安全カンファレンスの田口氏が共著

[kaizenさんの感想 · 2012年1月4日]

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

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

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

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

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

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

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

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

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

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

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

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

[H.Satoさんの感想 · 2010年3月2日]

モデル検査は、システム上起こりうる状態を網羅的に調べることによって設計誤りをは発見する自動検証手法の一つである。近年、高品質な検証ツールが開発、利用されている。