Merge

3 files changed, 59 insertions, 1 deletions

diff --git a/Jennisys/examples/List.jen b/Jennisys/examples/List.jen
index 184f4947..e7f42ddc 100644
--- a/Jennisys/examples/List.jen
+++ b/Jennisys/examples/List.jen
@@ -6,6 +6,9 @@ class List[T] {
 
   constructor Singleton(t: T)
     ensures list = [t]
+
+  constructor Double(p: T, q: T)
+    ensures list = [p q]
 }
 
 model List[T] {
@@ -27,6 +30,9 @@ class Node[T] {
 
   constructor Init(t: T)
     ensures list = [t]
+
+  constructor Double(p: T, q: T)
+    ensures list = [p q]
 }
 
 model Node[T] {
diff --git a/Jennisys/examples/List3.jen b/Jennisys/examples/List3.jen
index 6bb49eb8..acb10ad5 100644
--- a/Jennisys/examples/List3.jen
+++ b/Jennisys/examples/List3.jen
@@ -33,7 +33,7 @@ model IntList {
     root = null  ==> |list| = 0
     root != null ==> (|list| = |root.succ| + 1 && 
                       list[0] = root.data && 
-                      (forall i:int :: (0 <= i && i < |root.succ|) ==> (root.succ[i] != null && list[i+1] = root.succ[i].data)))
+                      (forall i:int :: (0 < i && i <= |root.succ|) ==> (root.succ[i-1] != null && list[i] = root.succ[i-1].data)))
 }
 
 class IntNode {
diff --git a/Jennisys/examples/Set.jen b/Jennisys/examples/Set.jen
new file mode 100644
index 00000000..6404bfd6
--- /dev/null
+++ b/Jennisys/examples/Set.jen
@@ -0,0 +1,52 @@
+class Set {
+  var elems: set[int]
+
+  constructor Empty()
+    ensures elems = {}
+
+  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}
+}
+
+model Set {
+  var root: SetNode
+
+  frame
+    root * root.elems[*]
+
+  invariant
+    root = null ==> elems = {}
+    root != null ==> elems = root.elems
+}
+
+class SetNode {
+  var elems: set[int]
+
+  constructor Init(t: int)
+    ensures elems = {t}
+
+  constructor Double(p: int, q: int)
+    requires p != q
+    ensures elems = {p q}
+}
+
+model SetNode {
+  var data: int
+  var left: SetNode
+  var right: SetNode
+
+  frame 
+    data * 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
+}