3.2 正しさの基準

3.2.1 正しさのいろいろ

(1) 証明条件

形式言語 →
- 構文が正しい
- 型が合ってる

P.56中～

状態ベース仕様 →
- 事後状態の存在
- 不変量

証明条件＝証明責務＝証明しなければならないもの

P.56下～

データに関する証明条件

P.57上～

操作に関する証明条件
≠アプリケーション性質

(2) 要求仕様に対する正しさ

ロジック・モデル検査 → システム記述＝検査仕様

P.57中～

状態ベース → システム記述≠検査仕様

なのでリファインメントが必要となる

[ex5-1] データに関する証明条件にあたるものはどれですか

[ex5-2] 操作に関する証明条件にあたるものはどれですか

3.2.2 型と型検査

型検査で実行前に間違いを見つけられる
＝記述の整合性をチェックできる

P.58上～

省略

3.2.3 状態ベース仕様の証明条件

• Condition->Action の解釈の違い

• 不変量の扱いの違い

(1) VDM-SLの証明条件

これにより操作の妥当性が担保される

P.59中～

P.59下～

前後ともに不変量が保たれる

P.59下～

P.60上～

(2)～(4)

省略

[ex5-3] 形式手法としての正しさのチェックに使わないものはどれですか

課題

教科書（図はすべてこちらより引用）：
　中島震，「形式手法入門―ロジックによるソフトウェア設計―」，オーム社