summaryrefslogtreecommitdiff
path: root/Jennisys/Jennisys/examples/oopsla12/BHeap.jen
diff options
context:
space:
mode:
Diffstat (limited to 'Jennisys/Jennisys/examples/oopsla12/BHeap.jen')
-rw-r--r--Jennisys/Jennisys/examples/oopsla12/BHeap.jen34
1 files changed, 0 insertions, 34 deletions
diff --git a/Jennisys/Jennisys/examples/oopsla12/BHeap.jen b/Jennisys/Jennisys/examples/oopsla12/BHeap.jen
deleted file mode 100644
index 41ebec85..00000000
--- a/Jennisys/Jennisys/examples/oopsla12/BHeap.jen
+++ /dev/null
@@ -1,34 +0,0 @@
-interface BHeap {
- var elems: set[int]
-
- constructor Singleton(x: int)
- elems := {x}
-
- constructor Dupleton(a: int, b: int)
- requires a != b
- elems := {a b}
-
- constructor Tripleton(x: int, y: int, z: int)
- requires x != y && y != z && z != x
- elems := {x y z}
-
- method Find(n: int) returns (ret: bool)
- 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}
-} \ No newline at end of file