4.2.2 模倣関係

(1) 前向き模倣

下向きと言っても良

abs;OpC ⊆ OpA;abs

P.74上～

模倣関係：
- 適切さ
- 初期化
- 適用可能性
- 正当性 ＝上の式

P.74中～

省略

(2) 関数的な前向き模倣

省略

(3) 後向き模倣

上向きと言っても良い

OpC;abs ⊆ abs;OpA

P.78下～

省略

[ex7-1] オペレーションの上位/下位の関係を調べる方法として前向き/後向き模倣の二種類を考えるのはなぜですか

(4) 前向き模倣と後向き模倣

片方だけでは不十分

P.81中～

P.81下～

前向き模倣：失敗

P.82上～

後向き模倣：成功

P.82中～

4.3 リファインメント検査

途中省略

4.3.2 Alloyとリファインメント

(3) 後方模倣の例題

座席が決まるタイミングが異なる

P.94下～

P.95上～

省略

P.97上～

(A)の前方模倣：成功

P.97下～

(B)の前方模倣：失敗
(B)の後方模倣：成功

P.98下～

決定的/非決定的の違い

[ex7-2] 前向き模倣になっているが後向き模倣にはなっていないケースはありますか

[ex7-3] 後向き模倣になっているが前向き模倣にはなっていないケースはありますか

[ex7-4] 前向き模倣と後向き模倣のどちらかになっていますか

課題

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