- added synthesis of Repr stuff (it generates Repr invariants,

   and updates the Repr fields at the end of every constructor)

 - refactoring:
    - removed ExprConst
    - change the implementation to use HeapModel and HeapInstance
      (as opposed to propagating heap/env/ctx)

4 files changed, 14 insertions, 9 deletions

diff --git a/Jennisys/examples/List.jen b/Jennisys/examples/List.jen
index e7f42ddc..63535a20 100644
--- a/Jennisys/examples/List.jen
+++ b/Jennisys/examples/List.jen
@@ -15,10 +15,10 @@ model List[T] {
   var root: Node[T]
 
   frame
-    root * root.list[*]
+    root
 
   invariant
-    (root = null) ==> (|list| = 0)
+    root = null ==> |list| = 0
     root != null ==> list = root.list
 }
 
@@ -40,7 +40,7 @@ model Node[T] {
   var next: Node[T]
 
   frame 
-    data * next
+    next
 
   invariant
     next = null <==> list = [data]
diff --git a/Jennisys/examples/List2.jen b/Jennisys/examples/List2.jen
index e99cf342..61fad148 100644
--- a/Jennisys/examples/List2.jen
+++ b/Jennisys/examples/List2.jen
@@ -27,7 +27,7 @@ model IntList {
   var root: IntNode
 
   frame
-    root * root.list[*]
+    root
 
   invariant
     root = null <==> |list| = 0
@@ -49,7 +49,7 @@ model IntNode {
   var next: IntNode
 
   frame 
-    data * next
+    next
 
   invariant
     next = null ==> list = [data]
diff --git a/Jennisys/examples/List3.jen b/Jennisys/examples/List3.jen
index acb10ad5..776bd43d 100644
--- a/Jennisys/examples/List3.jen
+++ b/Jennisys/examples/List3.jen
@@ -27,7 +27,7 @@ model IntList {
   var root: IntNode
 
   frame
-    root * root.list[*]
+    root
 
   invariant
     root = null  ==> |list| = 0
@@ -63,7 +63,7 @@ model IntNode {
   var next: IntNode
 
   frame 
-    data * next
+    next
 
   invariant
     next = null  ==> |succ| = 0
diff --git a/Jennisys/examples/Set.jen b/Jennisys/examples/Set.jen
index 6404bfd6..2142738e 100644
--- a/Jennisys/examples/Set.jen
+++ b/Jennisys/examples/Set.jen
@@ -13,13 +13,14 @@ class Set {
   constructor Double(p: int, q: int)
     requires p != q
     ensures elems = {p q}
+
 }
 
 model Set {
   var root: SetNode
 
   frame
-    root * root.elems[*]
+    root
 
   invariant
     root = null ==> elems = {}
@@ -35,6 +36,10 @@ class SetNode {
   constructor Double(p: int, q: int)
     requires p != q
     ensures elems = {p q}
+
+  constructor Triple(p: int, q: int, r: int)
+    requires p != q && q != r && r != p
+    ensures elems = {p q r}
 }
 
 model SetNode {
@@ -43,7 +48,7 @@ model SetNode {
   var right: SetNode
 
   frame 
-    data * left * right
+    left * right
 
   invariant
     elems = {data} + (left != null ? left.elems : {}) + (right != null ? right.elems : {})