4章 リファインメントを検査する

4.1 リファインメントとは

リファインメント：抽象レベルの異なる2つの仕様の関係

4.1.1 要求仕様とリファインメント

事後状態の存在や不変量の保存だけは足りない
→ リファインメント

P.67～

4.1.2 段階的な詳細化

(1) プログラム導出の方法

P.68下～

正しさを確認しながら詳細化を進める

P.69上～

例えば、抽象的に表現された操作を、プログラミング言語で具体化する

P.69中～

初期仕様が正しいこと前提

(2) 形式手法への導入

省略

[ex6-1] リファインメントに相当するのはどれですか

[ex6-2] 形式手法を用いて、正しさを確認しながら詳細化を進めたとしてもバグが残る原因はどれですか

4.1.3 段階的な機能追加

(1) モデリングの方法

詳細化：垂直リファインメント

機能追加：水平リファインメント

P.70中～

追加した機能が、既にあったものを壊してないことを確認

P.70下～

順序は任意

(2) Classical BとEvent-B

省略

4.2 リファインメントの基礎

4.2.1 2つの抽象レベル

[ex6-3] どちらに相当しますか：既に作り込んだ機能を保った上で新しい機能を作り込んだ

[ex6-4] どちらに相当しますか：形式仕様言語で書かれた仕様に基づきプログラミングを行なった

[ex6-5] あるオペレーションについて上位と下位の2つのレベルで考えるとき、考えるべき状態の数はいくつですか

課題

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