絵で描くオーバーライド


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