内容紹介
高品質のソフトウェアを効率よく開発する基礎知識が得られる
本書は、情報関連の大学学部学生およびソフトウェア技術者を対象に、高品質のソフトウェアを効率よく開発するための、プログラムの正しさを証明するためのプログラム検証理論と形式仕様記述を解説した。ソフトウェア開発におけるいわゆる形式手法の入門書である。
このような方におすすめ
情報関連学科でプログラミングの基礎を修得した大学学部学生・大学院生
ソフトウェア技術者
目次
主要目次
第1章 プログラムの正しさ－プログラムの検証入門－
第2章 Floyd-Hoare 論理
第3章 仕様としての事前条件と事後条件
第4章 VDM-SL による仕様記述の例
第5章 例題で見るシステム仕様記述
第6章 事例で見る実用的仕様記述
参考文献・関連ホームページ
付録
演習問題略解
詳細目次
第1章 プログラムの正しさ－プログラムの検証入門－
1.1 プログラムの正しさ
1.2 プログラムの正当性とその証明法 - 帰納的表明法 -
1.3 検証条件
1.4 プログラムの停止性
演習問題
第2章 Floyd-Hoare 論理
2.1 Floyd-Hoare 論理
2.2 配列要素への代入文
演習問題
第3章 仕様としての事前条件と事後条件
3.1 配列の整列プログラム
3.2 配列を用いるプログラムの部分的正当性の例
3.3 仕様記述の例
演習問題
第4章 VDM-SL による仕様記述の例
4.1 簡単な仕様記述の例
4.2 有用な基本データ型
演習問題
第5章 例題で見るシステム仕様記述
5.1 住所録
5.2 参加登録システム
演習問題
第6章 事例で見る実用的仕様記述
演習問題
参考文献・関連ホームページ
付録
A1. VDM-SL概説
A2. Zによる仕様記述
演習問題略解
続きを見る