驚くような三段論法

「抽象によるソフトウェア設計」を読んだ。
内容が難しい上にAlloyの記述形式に馴染めないので、読むのに時間が掛かった。
説明のための例としてアドレス帳を取り上げているのだが、アドレス帳の仕様記述には何の興味も湧かないので退屈だった。説明する側からすれば、ものすごく合理的で適切な例なんだろうと思うが。

抽象によるソフトウェア設計−Alloyではじめる形式手法−

付録に載っている練習問題を考えてみる。

A.3.1「驚くような三段論法」
Doris Dayの歌

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

これは「私は私の彼だ」を含意していることになる。検査せよ。

sig 人 {
  愛する: set 人
}
sig 彼 in 人 {}
one sig 私 in 人 {}

pred 歌の主張 {
  all x: 人 | 彼 in x.愛する                    -- Everybody loves my baby
  all b: 彼 | no (b.愛する & (人 - 私))     -- but my baby don’t love nobody but me.
}

fact { #彼 > 0 }
check { 歌の主張 => 私 in 彼 }

Solver=sat4j Bitwidth=0 MaxSeq=0 SkolemDepth=1 Symmetry=20
162 vars. 18 primary vars. 243 clauses. 114ms.
No counterexample found. Assertion may be valid. 11ms.

となって反例は見つからない。
fact {...}を消して、彼が存在しない場合も許すと、歌の主張に意味がなくなるので反例が生じる。