「形式手法入門」P22「2.1.3 抽象データの表現と解析」

非常に勉強になる本です。

多分、P25の命題のうち、2と4は、andじゃなくてimplies。

Stack.als

module Queue
abstract sig Node { next : lone Node }
abstract sig Queue { root : lone Node }

fact noCycle { no n : Node | n in n.^next }
fact noReflexive { no n : Node | n = n.next }
fact allNodeInAQueue {
	all n : Node | some q : Queue | n in q.root.*next
}

sig Stack extends Queue {}
fact hasBottom {
	all s : Stack | Bottom in (s.root).*next
}
sig Entry extends Node { value : Value - Empty }
fact entryHasNext {
	all e : Entry | one e.next
}
sig Bottom extends Node {}
fact bottomDontHaveNext { no Bottom.next }

sig Value {}
one sig Empty extends Value {}

pred empty [s1 : Stack ] { s1.root = Bottom }

pred push [s1, s2 : Stack, v : Value ] {
	some e1 : Entry |
		e1.value = v && e1.next = s1.root && s2.root = e1
}

pred pop [ s1, s2 : Stack] {
	(s1.root = Bottom) => s2.root = s1.root
					else s2.root = (s1.root).next
}

fun top [ s1 : Stack ] : Value {
	(s1.root = Bottom) => Empty else (s1.root).value
}

assert prop1 {
	all s1, s, s2 : Stack, v : Value |
		push[s1,s,v] and pop[s,s2] implies s1.root = s2.root
}

assert prop2 {
	all s1, s2 : Stack, v : Value |
		push[s1,s2,v] implies top[s2] = v
}

assert prop3 {
	all s1, s2 : Stack |
		empty[s1] and pop[s1,s2] implies s2.root = Bottom
}

assert prop4 {
	all s1 : Stack |
		empty[s1] implies top[s1] = Empty
}