A.3.1 驚くような三段論法 - Model Base

更新日2011-09-03
[ Alloy Analyzer ] / [ 抽象によるソフトウェア設計／付録 A 練習問題 解答例 ]

---

Doris Day の歌

Everybody loves my baby
but my baby don’t love nobody but me.

この歌をいくつかの制約で形式化し、Gries の推論をアサーションにせよ。

Doris Day の歌の主張を 述語DorisDay 、「私は私の彼だ」を 述語I_am_my_baby、Geriesの推論を示す 述語Gries は以下となる。

 pred Greies{
   DorisDay => I_am_my_baby
   }

"私"や、"私の彼"、"好き"などの構造を以下のように定義すると、

 sig Person{ 
   -- この人が愛している人達
   love: set Person
   }
 some sig MyBaby in Person{}
 one sig Me extends Person{}

述語DorisDay　と 述語I_am_my_baby は以下のようになる。

pred DorisDay{
   -- Everybody loves my baby
   all p: Person | MyBaby in p.love 
   -- but my baby don't love nobody but me.
   all p: Person | p=Me => (all b: MyBaby | p in b.love) else  p not in MyBaby.love 
   }
 
 pred I_am_my_baby{
   Me in MyBaby
   }
 
 assert Greies{ Greies }
 check Greies

アサーションを実行して反例は出なかった。

制約を変更して、Doris Day が言いたかったであろう形に記述し直し、今度はアサーションが反例を持つことを示せ

"Everybody loves my baby"の Everybody について、彼自身を除いてあげる。

 pred DorisDay'{
   -- Everybody loves my baby
   all p: Person-MyBaby | MyBaby in p.love 
   -- but my baby don't love nobody but me.
   all p: Person | p=Me => (all b: MyBaby | p in b.love) else  p not in MyBaby.love 
   }
 
 pred Greies'{
   DorisDay' => I_am_my_baby
   }
   
 assert Greies'{ Greies' }
 check Greies'

アサーションを実行して以下のような反例が出た。

---