3章 機能仕様を論理で考える

3.1 手続きとデータ構造

3.1.1 状態ベースの仕様

(1) モデル規範形式手法

モデル規範： プログラムを数学的な対象で表す

P.41下～

モデル規範 + 状態ベース仕様 が主流

(2) 状態間の関係

操作： 前状態と後状態の関係

P.42下～

不変条件： 状態がつねに満たすべき条件

P.43上～

(3) データ構造

状態はデータ構造で表わされる

P.43中～

P.43中～

複合データにはたいてい不変量がある

P.43下～

[ex4-1] まほろば掲示板を状態ベースでとらえるとして、状態に入れるべきでないものはどれですか

[ex4-2] まほろば掲示板での各掲示内容（文字列）を状態として注目したとき、これに関する不変条件はどれですか

[ex4-3] まほろば掲示板で、各掲示内容の残りの掲示日数（整数）に関する不変条件でないものはどれですか

3.1.2 例題による形式手法の比較

(1) Alloyによる記述（再考）

AddBirthday: エントリ追加

P.44下～

エントリを追加したけどknownに名前がない、というケースが問題

P.45上～

(b.birthday).Date = b.known

↑左辺： 関数(name, date) と (date) のジョイン → nameが残る

P.45下～

b : BirthdayBook を考えるときは、必ず birthdayPartial[b] でなければならない

P.46上～

not(n in b.known)

追加しようとする人が既にあってはいけない

P.46中～

3.1.3 形式手法の比較

(1) VDM-SL

P.47下～

Alloyと違って更新する変数を明示(wr)する

P.4?上～

VDM-SLではinvで不変条件を書ける

P.48中～

(2)～(4)

省略

3.1.4 2つの解釈

契約として解釈： Condition ならば Action という命題が成立してる

↓

Conditionが偽のときはどうなる？

P.53下～

振る舞い解釈： Condition が真のとき Action が実行される

[ex4-4] 教科書のBirthdayBookについて、エントリを削除する操作を記述したいときに無関係なものはどれですか

[ex4-5] VDM-SLのようにwrやinvなど、Alloyにない構文があればより便利ですが、その反面のデメリットは何ですか

課題

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