1 files changed, 34 insertions, 0 deletions
diff --git a/Source/Jennisys/examples/oopsla12/BHeap.jen b/Source/Jennisys/examples/oopsla12/BHeap.jen
new file mode 100644
index 00000000..41ebec85
--- /dev/null
+++ b/Source/Jennisys/examples/oopsla12/BHeap.jen
@@ -0,0 +1,34 @@
+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