1 files changed, 0 insertions, 72 deletions
diff --git a/Jennisys/Jennisys/examples/Set.jen b/Jennisys/Jennisys/examples/Set.jen
deleted file mode 100644
index 01532f96..00000000
--- a/Jennisys/Jennisys/examples/Set.jen
+++ /dev/null
@@ -1,72 +0,0 @@
-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
-}