絵で描くオーバーライド
sig X{} sig Y{} pred p[r1, r2: X -> Y]{ #r1 < 3 #r2 < 3 (r1 + r2) != (r1 ++ r2) (r1 ++ r2) != (r2 ++ r1) (r2 ++ r1) != (r1 + r2) no r1 & iden no r2 & iden } run p for 4 int
Alloyは「条件を満たす小さい事例を探す」ってタスクには抜群の使いやすさを発揮するな。
r1, r2, r1 + r2, r1 ++ r2, r2 ++ r1がそれぞれ異なる小さい例。ちなみにXが2個以下では例がなく、Yが2個以下だと6通りある。
sig X{} sig Y{} pred p[r1, r2: X -> Y]{ #r1 < 3 #r2 < 3 (r1 + r2) != (r1 ++ r2) (r1 ++ r2) != (r2 ++ r1) (r2 ++ r1) != (r1 + r2) (r1 + r2) != r1 (r1 ++ r2) != r1 (r2 ++ r1) != r1 (r1 + r2) != r2 (r1 ++ r2) != r2 (r2 ++ r1) != r2 no r1 & iden no r2 & iden } run p for 4 int