diff options
Diffstat (limited to 'Source/Jennisys/examples/BHeap.jen')
-rw-r--r-- | Source/Jennisys/examples/BHeap.jen | 33 |
1 files changed, 33 insertions, 0 deletions
diff --git a/Source/Jennisys/examples/BHeap.jen b/Source/Jennisys/examples/BHeap.jen new file mode 100644 index 00000000..55258bde --- /dev/null +++ b/Source/Jennisys/examples/BHeap.jen @@ -0,0 +1,33 @@ +interface BHeap { + var elems: set[int] + + constructor Singleton(x: int) + ensures elems = {x} + + constructor Dupleton(a: int, b: int) + requires a != b + ensures elems = {a b} + + constructor Tripleton(x: int, y: int, z: int) + requires x != y && y != z && z != x + ensures elems = {x y z} + + method Find(n: int) returns (ret: bool) + ensures ret = (n in elems) +} + +datamodel BHeap { + var data: int + var left: BHeap + var right: BHeap + + frame + 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 + left = null ==> right = null + (left != null && right = null) ==> left.elems = {left.data} +} |