本棚登録 : 
感想 : 
- Amazon.co.jp ・本 (191ページ)
- / ISBN・EAN: 9784274132636
作品紹介・あらすじ
本書は、ソフトウェア開発におけるいわゆる形式手法(formal methods)の入門書である。プログラムの正しさを証明するためのプログラム検証理論と形式仕様記述との初歩を紹介している。
感想・レビュー・書評
-
コメント0件をすべて表示
-
【書誌情報】
『プログラム仕様記述論』
著者：荒木 啓二郎［あらき・けいじろう］
著者：張 漢明 ［ちょう・かんめい］
シリーズ著者：情報処理学会
シリーズ名：IT text
定価：3,080円 （本体2,800円＋税）
判型：A5
頁：210頁
ISBN：978-4-274-13263-6
発売日：2002/11/22
発行元：オーム社
本書は、情報関連の大学学部学生およびソフトウェア技術者を対象に、高品質のソフトウェアを効率よく開発するための、プログラムの正しさを証明するためのプログラム検証理論と形式仕様記述を解説した。ソフトウェア開発におけるいわゆる形式手法の入門書である。
〈https://www.ohmsha.co.jp/book/9784274132636/〉
【簡易目次】
はしがき [iii-v]
本書の構成と活用法 [vii-xi]
目次 [xiii-xvi]
第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章 事例で見る実用的仕様記述
演習問題
付録A VDM-SL概説
A.1 データ型（Data Type Definitions） 153
A.2 構文概要 158
付録B Zによる仕様記述
B.1 Zの概説 166
B.2 住所録システム 168
B.3 参加登録システム 170
B.4 自動販売機 173
演習問題略解 [175-180]
参考文献・関連ホームページ [181-185]
索引 [187-191]
【目次】
第1章 プログラムの正しさ - プログラムの検証入門
1.1 ブログラムの正しさ
1.2 ブログラムの正当性とその証明法一帰納的表明法……6
1. 正しさの基準としての事前条件と事後条件
2. 帰納的表明 7
1.3 検証条件...12
1. 流れ図プログラムに対する規則 12
2. 部分的正当性の証明例 15
1.4 プログラムの停止性
1. 停止性の証明 18
2. 停止性の証明例 19
演習問題 21
第2章 Floyd-Hoare 論理
2.1 Floyd-Hoare 論理
1. 論理式としての部分的正当性の表明
2. 部分的正当性の証明体系 25
3. 例題 29
2.2 配列要素への代入文
1. 配列要素への代入文の公理 37
演習問題 42
第3章 仕様としての事前条件と事後条件 45
3.1 配列の整列プログラム
1. 仕様の書き方
2. より適切な仕様
3.3 仕様記述の例
3.2 配列を用いるプログラムの部分的正当性の例
演習問題 61
第4章 VDM-SL による仕様記述の例
4.1 簡単な仕様記述の例
4.2 有用な基本データ型
1. 集合型79
2.列型84
3. 写像型 90
4. 直積型 97
5. 複合型 99
演習問題 101
第5章 例題で見るシステム仕様記述
5.1 住所録システム
1. 形式的な仕様記述の基本概念 104
2. エラー処理の記述 108
3. 事前条件と事後条件による仕様記述
4. 状態に基づくモデリング 113
5.2 参加登録システム
1. 単純なモデル 116
2. 情報の整理 120
3. 情報の詳細化 126
4. 複雑なシステムの記述 129
演習問題 132
第6章 事例で見る実用的仕様記述
6.1 対象とする自動販売機
6.2 自動販売機の抽象モデル
1. 状態定義 137
2. 操作定義
3. 関数を用いた操作の再定義
6.3 モデルの拡張:ランプの導入
1. 状態定義 143
2. 関数定義 145
3. 操作定義 146
6.4 具体化:ボタンとカラムの導入
1. 状態定義 147
2. 関数定義 150
3. 操作定義 152
演習問題 152
付録A VDM-SL概説
A.1 データ型(Data Type Definitions)
1. 基本データ型(Basic Data Types)
2. 合成型(Compound Types) 156
A.2 構文概要
1. 定義ブロック 158
2. 型定義 159
3. 状態定義 160
4. 値定義 160
5. 関数定義、 160
6. 操作定義 160
7. 式 161
8. パターン 164
9. 束縛 164
付録 B zによる仕様記述.....166
B.1 Zの概説
1. スキーマ 166
2. データ定義 166
3. 状態スキーマ 166
4. 操作スキーマ 167
B.2 住所録システム
1. 型定義 168
2. 状態定義
3.操作定義
B.3 参加登錄
1. 型定義
2. 状態定義
3.操作定義
B.4 自動販売機
0
