P25の「代数的な性質の検査」の4条件のうち、2と4はandじゃなくてimpliesになるのでは。
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 }