summaryrefslogtreecommitdiff
path: root/Jennisys/examples/Set.jen
diff options
context:
space:
mode:
Diffstat (limited to 'Jennisys/examples/Set.jen')
-rw-r--r--Jennisys/examples/Set.jen9
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 : {})