diff options
author | 2011-07-11 19:09:41 -0700 | |
---|---|---|
committer | 2011-07-11 19:09:41 -0700 | |
commit | 1dd0047d2bb46b64a4d04259ba7803fc09898194 (patch) | |
tree | 554bf9b30251a62c258a221343936f25e17cd51a /Jennisys/examples/Set.jen | |
parent | eacaf0b44276f0a61d6cc4204bb4d48d02fc0548 (diff) | |
parent | 61acaf623c5acf36b57d958e788f10f3c23bd309 (diff) |
Merge
Diffstat (limited to 'Jennisys/examples/Set.jen')
-rw-r--r-- | Jennisys/examples/Set.jen | 52 |
1 files changed, 52 insertions, 0 deletions
diff --git a/Jennisys/examples/Set.jen b/Jennisys/examples/Set.jen new file mode 100644 index 00000000..6404bfd6 --- /dev/null +++ b/Jennisys/examples/Set.jen @@ -0,0 +1,52 @@ +class Set { + var elems: set[int] + + constructor Empty() + ensures elems = {} + + constructor Singleton(t: int) + ensures elems = {t} + + constructor Sum(p: int, q: int) + ensures elems = {p + q} + + constructor Double(p: int, q: int) + requires p != q + ensures elems = {p q} +} + +model Set { + var root: SetNode + + frame + root * root.elems[*] + + invariant + root = null ==> elems = {} + root != null ==> elems = root.elems +} + +class SetNode { + var elems: set[int] + + constructor Init(t: int) + ensures elems = {t} + + constructor Double(p: int, q: int) + requires p != q + ensures elems = {p q} +} + +model SetNode { + var data: int + var left: SetNode + var right: SetNode + + frame + data * left * right + + invariant + elems = {data} + (left != null ? left.elems : {}) + (right != null ? right.elems : {}) + left != null ==> forall e :: e in left.elems ==> e < data + right != null ==> forall e :: e in right.elems ==> e > data +} |