1 files changed, 72 insertions, 0 deletions
diff --git a/Source/Jennisys/examples/Set.jen b/Source/Jennisys/examples/Set.jen
new file mode 100644
index 00000000..01532f96
--- /dev/null
+++ b/Source/Jennisys/examples/Set.jen
@@ -0,0 +1,72 @@
+interface Set {
+  var elems: set[int]
+
+  constructor Empty()
+    ensures elems = {}
+
+  constructor SingletonZero()
+    ensures elems = {0}
+
+  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}
+
+}
+
+datamodel Set {
+  var root: SetNode
+
+  frame
+    root
+
+  invariant
+    root = null ==> elems = {}
+    root != null ==> elems = root.elems
+}
+
+interface SetNode {
+  var elems: set[int]
+
+  constructor Init(x: int)
+    ensures elems = {x}
+
+  constructor Double(a: int, b: int)
+    requires a != b
+    ensures elems = {a b}
+
+  constructor DoubleBase(x: int, y: int)
+    requires x > y
+    ensures elems = {x y}
+
+  constructor Triple(x: int, y: int, z: int)
+    requires x != y && y != z && z != x
+    ensures elems = {x y z}
+
+  constructor TripleBase(x: int, y: int, z: int)
+    requires x < y && y < z
+    ensures elems = {x y z}
+	
+  method Find(n: int) returns (ret: bool)
+    ensures ret = (n in elems)
+	
+}
+
+datamodel SetNode {
+  var data: int
+  var left: SetNode
+  var right: SetNode
+
+  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
+}