1 files changed, 30 insertions, 0 deletions
diff --git a/Source/Jennisys/examples/oopsla12/IntSet.jen b/Source/Jennisys/examples/oopsla12/IntSet.jen
new file mode 100644
index 00000000..4800371e
--- /dev/null
+++ b/Source/Jennisys/examples/oopsla12/IntSet.jen
@@ -0,0 +1,30 @@
+interface IntSet {
+  var elems: set[int]             
+
+  constructor Singleton(x: int)
+    elems := {x}
+
+  constructor Dupleton(x: int, y: int)
+    requires x != y
+    elems := {x y}
+
+  method Find(x: int) returns (ret: bool)
+    ret := x in elems
+}
+
+datamodel IntSet {
+  var data: int
+  var left: IntSet
+  var right: IntSet
+  
+  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 ==> data < e)
+} 
+\ No newline at end of file