diff options
Diffstat (limited to 'Jennisys/examples/Set.jen')
-rw-r--r-- | Jennisys/examples/Set.jen | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/Jennisys/examples/Set.jen b/Jennisys/examples/Set.jen index 6404bfd6..2142738e 100644 --- a/Jennisys/examples/Set.jen +++ b/Jennisys/examples/Set.jen @@ -13,13 +13,14 @@ class Set { constructor Double(p: int, q: int) requires p != q ensures elems = {p q} + } model Set { var root: SetNode frame - root * root.elems[*] + root invariant root = null ==> elems = {} @@ -35,6 +36,10 @@ class SetNode { constructor Double(p: int, q: int) requires p != q ensures elems = {p q} + + constructor Triple(p: int, q: int, r: int) + requires p != q && q != r && r != p + ensures elems = {p q r} } model SetNode { @@ -43,7 +48,7 @@ model SetNode { var right: SetNode frame - data * left * right + left * right invariant elems = {data} + (left != null ? left.elems : {}) + (right != null ? right.elems : {}) |