1 files changed, 0 insertions, 60 deletions
diff --git a/Jennisys/Jennisys/examples/Set2.jen b/Jennisys/Jennisys/examples/Set2.jen
deleted file mode 100644
index cfbcbce7..00000000
--- a/Jennisys/Jennisys/examples/Set2.jen
+++ /dev/null
@@ -1,60 +0,0 @@
-class Set {  var elems: seq[int]
-
-  constructor Empty()
-    ensures elems = []
-
-  constructor Singleton(t: int)
-    ensures elems = [t]
-
-  constructor Sum(p: int, q: int)
-    ensures elems = [p + q]
-
-}
-
-model Set {
-  var root: SetNode
-
-  frame
-    root
-
-  invariant
-    root = null ==> elems = []
-    root != null ==> elems = root.elems
-}
-
-class SetNode {
-  var elems: seq[int]
-
-  constructor Init(x: int)
-    ensures elems = [x]
-
-  constructor Double(a: int, b: int)
-    requires a != b
-    ensures |elems| = 2 && a in elems && b in elems
-
-  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| = 3 && x in elems && y in elems && z in elems
-
-  constructor TripleBase(x: int, y: int, z: int)
-    requires x < y && y < z
-    ensures elems = [x y z]
-}
-
-model SetNode {
-  var data: int
-  var left: SetNode
-  var right: SetNode
-
-  frame 
-    left * right
-
-  invariant
-    elems = (left != null ? left.elems : []) + [data] + (right != null ? right.elems : [])
-    left != null  ==> forall e :: e in left.elems ==> e < data
-    right != null ==> forall e :: e in right.elems ==> e > data
-}