1 files changed, 0 insertions, 71 deletions
diff --git a/Jennisys/Jennisys/examples/List3.jen b/Jennisys/Jennisys/examples/List3.jen
deleted file mode 100644
index 9130f82a..00000000
--- a/Jennisys/Jennisys/examples/List3.jen
+++ /dev/null
@@ -1,71 +0,0 @@
-interface IntList {
-  var list: seq[int]
-
-  constructor Empty()
-    ensures list = []
-
-  constructor SingletonTwo()
-    ensures list = [2]
-
-  constructor OneTwo()
-    ensures list = [1 2]
-
-  constructor Singleton(p: int)
-    ensures list = [p]
-
-  constructor TwoConsecutive(p: int)
-    ensures list = [p] + [p+1]
-
-  constructor Double(p: int, q: int)
-    ensures list = [p] + [q]
-
-  constructor Sum(p: int, q: int)
-    ensures list = [p + q]
-}
-
-datamodel IntList {
-  var root: IntNode
-
-  frame
-    root
-
-  invariant
-    root = null  ==> |list| = 0
-    root != null ==> (|list| = |root.succ| + 1 && 
-                      list[0] = root.data && 
-                      (forall i :: i in 1 ... |root.succ| ==> (root.succ[i-1] != null && list[i] = root.succ[i-1].data)))
-}
-
-interface IntNode {
-  var succ: seq[IntNode]
-  var data: int
-
-  constructor Zero()
-    ensures data = 0
-    ensures succ = []
-
-  constructor OneTwo()
-    ensures data = 1
-    ensures |succ| = 1 && succ[0] != null && succ[0].data = 2
-
-  constructor Init(p: int)
-    ensures data = p
-
-  constructor InitInc(p: int)
-    ensures data = p + 1
-
-    
-  invariant
-    !(null in succ)
-}
-
-datamodel IntNode {
-  var next: IntNode
-
-  frame 
-    next
-
-  invariant
-    next = null  ==> |succ| = 0
-    next != null ==> (succ = [next] + next.succ)
-}