2章 指先で考える

2.1 Alloy入門

2.1.1 Alloyの面白さ

有限モデルに限定して自動検査する

2.1.2 Compositeパターン

(1) Alloy記述の基本

module Composite

abstract sig Component {}
sig Composite extends Component {
children : set Component
}
sig Leaf extends Component {}

P.15上～

P.15下～

• childrenが自分自身

• 親が2つある

(2) 制約条件の追加

P.17上～

性質1をnoRefferedToとonlyRootで表現

P.17下～

性質2をsingleWholeで表現

P.18中～

求めるものに近付いた

(3) 表明の検査

show2[] implies noSelfLoop[]

(4) 書き方の補足説明

abstractの説明

P.20上～

pred vs fact

P.20中～ 省略

[ex2-1] Alloyが有限モデルに限定して検査するのはなぜですか

[ex2-2] プログラミング言語にはあてはまり、Alloyコードにはあてはまらないものはどれですか

2.1.3 抽象データの表現と解析

スタックを表現する

(1) キューの定義

abstract sig Node { next : lone Node }
abstract sig Queue { root : lone Node }

(2) スタックの定義と動作の確認

P.23下～

pred empty ( s1 : Stack ) { s1.root = Bottom }

P.24中～

push, pop

P.24下～

top(読み出し)

P.25上～

empty → push → pop したらどうなるか？

(3) 代数的に性質の検査

検査内容もできるだけ抽象的に書きたい

P.25下～

1. pushしてpopしたら元に戻る

P.25下～

2.1.4 機能仕様の表現と解析

BirthdayBook

（省略）

[ex2-3] スタックの検査としてより抽象度が高いのはどちらですか

[ex2-4] スタックの検査としてより抽象度が高いのはどちらですか

課題

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