1 files changed, 0 insertions, 68 deletions
diff --git a/Jennisys/Jennisys/examples/List2.jen b/Jennisys/Jennisys/examples/List2.jen
deleted file mode 100644
index 3bd527fb..00000000
--- a/Jennisys/Jennisys/examples/List2.jen
+++ /dev/null
@@ -1,68 +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.list
-}
-
-interface IntNode {
-  var list: seq[int]
-
-  invariant
-    |list| > 0
-
-  constructor SingletonZero()
-    ensures list = [0]
-
-  constructor Init(x: int) 
-    ensures list = [x]
-
-  constructor Double(x: int, y: int)
-    ensures list = [x y]
-	
-  method Max() returns (ret: int)
-    ensures ret in list
-	ensures forall t :: t in list ==> ret >= t
-
-}
-
-datamodel IntNode {
-  var data: int
-  var next: IntNode
-
-  frame 
-    next
-
-  invariant
-    next = null ==> list = [data]
-    next != null ==> list = [data] + next.list
-}