Model Base
A.3.1 驚くような三段論法
最終更新:
modelbase
更新日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'
アサーションを実行して以下のような反例が出た。