Put all sources under \Source directory

38 files changed, 6073 insertions, 0 deletions

diff --git a/Source/Jennisys/examples/BHeap.jen b/Source/Jennisys/examples/BHeap.jen
new file mode 100644
index 00000000..55258bde
--- /dev/null
+++ b/Source/Jennisys/examples/BHeap.jen
@@ -0,0 +1,33 @@
+interface BHeap {
+  var elems: set[int]
+
+  constructor Singleton(x: int)
+    ensures elems = {x}
+
+  constructor Dupleton(a: int, b: int)
+    requires a != b
+    ensures elems = {a b}
+
+  constructor Tripleton(x: int, y: int, z: int)
+    requires x != y && y != z && z != x
+    ensures elems = {x y z}
+
+  method Find(n: int) returns (ret: bool)
+    ensures ret = (n in elems)	
+}
+
+datamodel BHeap {
+  var data: int
+  var left: BHeap
+  var right: BHeap
+
+  frame 
+    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
+	left = null ==> right = null
+	(left != null && right = null) ==> left.elems = {left.data}
+} 
diff --git a/Source/Jennisys/examples/DList.jen b/Source/Jennisys/examples/DList.jen
new file mode 100644
index 00000000..43337ca8
--- /dev/null
+++ b/Source/Jennisys/examples/DList.jen
@@ -0,0 +1,39 @@
+interface DNode[T] {

+  var list: seq[T]

+

+  invariant

+    |list| > 0

+

+  constructor Init(t: T)

+    ensures list = [t]

+

+  constructor Double(p: T, q: T)

+    ensures list = [p q]

+

+  method List() returns (ret: seq[T])

+    ensures ret = list

+

+  method Size() returns (ret: int)

+    ensures ret = |list|

+

+  method Get(idx: int) returns (ret: T)

+    requires idx >= 0 && idx < |list|

+    ensures ret = list[idx]

+

+  method Find(n: T) returns (ret: bool)

+    ensures ret = (n in list)

+}

+

+datamodel DNode[T] {

+  var data: T

+  var next: DNode[T]

+  var prev: DNode[T]

+  

+  frame 

+    next

+

+  invariant

+    next = null ==> list = [data]

+    next != null ==> (list = [data] + next.list  &&  next.prev = this)

+	prev != null ==> prev.next = this

+} 

diff --git a/Source/Jennisys/examples/List.jen b/Source/Jennisys/examples/List.jen
new file mode 100644
index 00000000..85a3b692
--- /dev/null
+++ b/Source/Jennisys/examples/List.jen
@@ -0,0 +1,77 @@
+interface List[T] {
+  var list: seq[T]
+
+  constructor Empty()
+    ensures list = []
+
+  constructor Singleton(t: T)
+    ensures list = [t]
+
+  constructor Double(p: T, q: T)
+    ensures list = [p q]
+}
+
+datamodel List[T] {
+  var root: Node[T]
+
+  frame
+    root
+
+  invariant
+    root = null ==> |list| = 0
+    root != null ==> list = root.list
+}
+
+interface Node[T] {
+  var list: seq[T]
+
+  invariant
+    |list| > 0
+
+  constructor Init(t: T)
+    ensures list = [t]
+
+  constructor Double(p: T, q: T)
+    ensures list = [p q]
+
+  method List() returns (ret: seq[T])
+    ensures ret = list
+
+  method Tail() returns (tail: Node[T])
+    ensures |list| = 1 ==> tail = null
+    ensures |list| > 1 ==> tail != null && tail.list = list[1..]
+
+  method Size() returns (ret: int)
+    ensures ret = |list|
+
+  method SkipFew(num: int) returns (ret: Node[T])
+    requires num >= 0
+    ensures num >= |list| ==> ret = null
+    ensures num < |list| ==> ret != null && ret.list = list[num..]
+
+  method Get(idx: int) returns (ret: T)
+    requires idx >= 0 && idx < |list|
+    ensures ret = list[idx]
+
+  method Index(n: T) returns (ret: int)
+    ensures n !in list ==> ret = -1
+    ensures n in list ==> ret >= 0 && ret < |list| && list[ret] = n
+
+  method Find(n: T) returns (ret: bool)
+    ensures ret = (n in list)
+	
+  method Insert(n: T) 
+    ensures list = old(list) + [n]  
+}
+
+datamodel Node[T] {
+  var data: T
+  var next: Node[T]
+
+  frame 
+    next
+
+  invariant
+    next = null ==> list = [data]
+    next != null ==> list = [data] + next.list 
+} 
diff --git a/Source/Jennisys/examples/List2.jen b/Source/Jennisys/examples/List2.jen
new file mode 100644
index 00000000..3bd527fb
--- /dev/null
+++ b/Source/Jennisys/examples/List2.jen
@@ -0,0 +1,68 @@
+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
+} 
diff --git a/Source/Jennisys/examples/List3.jen b/Source/Jennisys/examples/List3.jen
new file mode 100644
index 00000000..9130f82a
--- /dev/null
+++ b/Source/Jennisys/examples/List3.jen
@@ -0,0 +1,71 @@
+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)
+} 
diff --git a/Source/Jennisys/examples/Number.jen b/Source/Jennisys/examples/Number.jen
new file mode 100644
index 00000000..e31613bd
--- /dev/null
+++ b/Source/Jennisys/examples/Number.jen
@@ -0,0 +1,44 @@
+interface Number { 
+  var num: int
+ 
+  constructor Init(p: int)
+    ensures num = p
+
+  constructor Double(p: int)
+    ensures num = 2*p
+
+  constructor Sum(a: int, b: int)
+    ensures num = a + b
+
+  constructor Min2(a: int, b: int)
+    ensures a < b ==> num = a
+    ensures a >= b ==> num = b
+
+  constructor Min22(a: int, b: int)
+    ensures num in {a b}
+    ensures num <= a && num <= b
+
+  constructor Min3(a: int, b: int, c: int)
+    ensures num in {a b c}
+    ensures num <= a && num <= b && num <= c
+
+  constructor Min32(a: int, b: int, c: int)
+    ensures num in {a b c}
+    ensures forall x :: x in {a b c} ==> num <= x
+
+  constructor MinSum(a: int, b: int, c: int)
+    ensures num in {a+b a+c b+c}
+    ensures num <= a+b && num <= b+c && num <= a+c
+
+  constructor Min4(a: int, b: int, c: int, d: int)
+    ensures num in {a b c d}
+    ensures forall x :: x in {a b c d} ==> num <= x
+
+  constructor Abs(a: int)  
+    ensures num in {a (-a)} && num >= 0
+
+}
+
+datamodel Number {
+
+}
\ No newline at end of file
diff --git a/Source/Jennisys/examples/NumberMethods.jen b/Source/Jennisys/examples/NumberMethods.jen
new file mode 100644
index 00000000..f9b17f74
--- /dev/null
+++ b/Source/Jennisys/examples/NumberMethods.jen
@@ -0,0 +1,40 @@
+interface NumberMethods {
+ 
+  method Double(p: int) returns (ret: int)
+    ensures ret = 2*p
+
+  method Sum(a: int, b: int) returns (ret: int)
+    ensures ret = a + b
+
+  method Min2(a: int, b: int) returns (ret: int)
+    ensures a < b ==> ret = a
+    ensures a >= b ==> ret = b
+
+  method Min22(a: int, b: int) returns (ret: int)
+    ensures ret in {a b}
+    ensures ret <= a && ret <= b
+
+  method Min3(a: int, b: int, c: int) returns (ret: int)
+    ensures ret in {a b c}
+    ensures ret <= a && ret <= b && ret <= c
+
+  method Min32(a: int, b: int, c: int) returns (ret: int)
+    ensures ret in {a b c}
+    ensures forall x :: x in {a b c} ==> ret <= x
+
+ method MinSum(a: int, b: int, c: int) returns (ret: int)
+    ensures ret in {a+b a+c b+c}
+    ensures ret <= a+b && ret <= b+c && ret <= a+c
+
+ method Min4(a: int, b: int, c: int, d: int) returns (ret: int)
+    ensures ret in {a b c d}
+    ensures forall x :: x in {a b c d} ==> ret <= x
+
+  method Abs(a: int) returns (ret: int)
+    ensures ret in {a (-a)} && ret >= 0
+
+}
+
+datamodel NumberMethods {
+
+}
\ No newline at end of file
diff --git a/Source/Jennisys/examples/Set.jen b/Source/Jennisys/examples/Set.jen
new file mode 100644
index 00000000..01532f96
--- /dev/null
+++ b/Source/Jennisys/examples/Set.jen
@@ -0,0 +1,72 @@
+interface Set {
+  var elems: set[int]
+
+  constructor Empty()
+    ensures elems = {}
+
+  constructor SingletonZero()
+    ensures elems = {0}
+
+  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}
+
+}
+
+datamodel Set {
+  var root: SetNode
+
+  frame
+    root
+
+  invariant
+    root = null ==> elems = {}
+    root != null ==> elems = root.elems
+}
+
+interface SetNode {
+  var elems: set[int]
+
+  constructor Init(x: int)
+    ensures elems = {x}
+
+  constructor Double(a: int, b: int)
+    requires a != b
+    ensures elems = {a b}
+
+  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 = {x y z}
+
+  constructor TripleBase(x: int, y: int, z: int)
+    requires x < y && y < z
+    ensures elems = {x y z}
+	
+  method Find(n: int) returns (ret: bool)
+    ensures ret = (n in elems)
+	
+}
+
+datamodel SetNode {
+  var data: int
+  var left: SetNode
+  var right: SetNode
+
+  frame 
+    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
+} 
diff --git a/Source/Jennisys/examples/Set2.jen b/Source/Jennisys/examples/Set2.jen
new file mode 100644
index 00000000..cfbcbce7
--- /dev/null
+++ b/Source/Jennisys/examples/Set2.jen
@@ -0,0 +1,60 @@
+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
+} 
diff --git a/Source/Jennisys/examples/Simple.jen b/Source/Jennisys/examples/Simple.jen
new file mode 100644
index 00000000..2f5e7feb
--- /dev/null
+++ b/Source/Jennisys/examples/Simple.jen
@@ -0,0 +1,31 @@
+interface Simple {

+ var a: int

+ 

+ method Inc(p: int)

+   a := old(a) + p   

+   

+ method Init(n: int)

+   a := n

+   

+ method Max(x: int, y: int)

+   ensures x < y ==> a = y

+   ensures x >= y ==> a = x

+   

+ 

+ method Max2(x: int, y: int)

+   ensures a = x || a = y

+   ensures forall t :: t in {x y} ==> a >= t

+   

+ method Max3__mod__(x: int, y: int)

+   ensures a in {x y}

+   ensures forall t :: t in {x y} ==> a >= t   

+   

+ method MaxAll__mod__(x: seq[int])

+   ensures a in x

+   ensures forall t :: t in x ==> a >= t

+}

+

+datamodel Simple {

+ var c: int

+ invariant a = c

+}
\ No newline at end of file
diff --git a/Source/Jennisys/examples/jennisys-synth_List.dfy b/Source/Jennisys/examples/jennisys-synth_List.dfy
new file mode 100644
index 00000000..0611c78b
--- /dev/null
+++ b/Source/Jennisys/examples/jennisys-synth_List.dfy
@@ -0,0 +1,147 @@
+class List<T> {

+  ghost var Repr: set<object>;

+  ghost var list: seq<T>;

+

+  var root: Node<T>;

+

+  function Valid_repr(): bool

+    reads *;

+  {

+    this in Repr &&

+    null !in Repr &&

+    (root != null ==> root in Repr && root.Repr <= Repr && this !in root.Repr)

+  }

+

+  function Valid_self(): bool

+    reads *;

+  {

+    Valid_repr() &&

+    (root == null ==> |list| == 0) &&

+    (root != null ==> list == root.list)

+  }

+

+  function Valid(): bool

+    reads *;

+  {

+    this.Valid_self() &&

+    (root != null ==> root.Valid())

+  }

+

+  method Empty()

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures list == [];

+  {

+    this.list := [];

+    this.root := null;

+    // repr stuff

+    this.Repr := {this};

+  }

+

+  method Singleton(t: T)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures list == [t];

+  {

+    var gensym65 := new Node<T>;

+    gensym65.data := t;

+    gensym65.list := [t];

+    gensym65.next := null;

+    this.list := [t];

+    this.root := gensym65;

+    // repr stuff

+    gensym65.Repr := {gensym65};

+    this.Repr := {this} + this.root.Repr;

+  }

+

+  method Double(p: T, q: T)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures list == [p, q];

+  {

+    var gensym66 := new Node<T>;

+    var gensym67 := new Node<T>;

+    gensym66.data := p;

+    gensym66.list := [p, q];

+    gensym66.next := gensym67;

+    gensym67.data := q;

+    gensym67.list := [q];

+    gensym67.next := null;

+    this.list := [p, q];

+    this.root := gensym66;

+    // repr stuff

+    gensym67.Repr := {gensym67};

+    gensym66.Repr := {gensym66} + gensym66.next.Repr;

+    this.Repr := {this} + this.root.Repr;

+  }

+

+}

+

+class Node<T> {

+  ghost var Repr: set<object>;

+  ghost var list: seq<T>;

+

+  var data: T;

+  var next: Node<T>;

+

+  function Valid_repr(): bool

+    reads *;

+  {

+    this in Repr &&

+    null !in Repr &&

+    (next != null ==> next in Repr && next.Repr <= Repr && this !in next.Repr)

+  }

+

+  function Valid_self(): bool

+    reads *;

+  {

+    Valid_repr() &&

+    (next == null <==> list == [data] && list[0] == data) &&

+    (next != null ==> list == [data] + next.list) &&

+    (|list| > 0)

+  }

+

+  function Valid(): bool

+    reads *;

+  {

+    this.Valid_self() &&

+    (next != null ==> next.Valid_self() && (next.next != null ==> next.next.Valid_self()))

+  }

+

+  method Init(t: T)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures list == [t];

+  {

+    this.data := t;

+    this.list := [t];

+    this.next := null;

+    // repr stuff

+    this.Repr := {this};

+  }

+

+  method Double(p: T, q: T)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures list == [p, q];

+  {

+    var gensym71 := new Node<T>;

+    gensym71.data := q;

+    gensym71.list := [q];

+    gensym71.next := null;

+    this.data := p;

+    this.list := [p, q];

+    this.next := gensym71;

+    // repr stuff

+    gensym71.Repr := {gensym71};

+    this.Repr := {this} + this.next.Repr;

+  }

+

+}

+

+

diff --git a/Source/Jennisys/examples/jennisys-synth_List2.dfy b/Source/Jennisys/examples/jennisys-synth_List2.dfy
new file mode 100644
index 00000000..13e521a8
--- /dev/null
+++ b/Source/Jennisys/examples/jennisys-synth_List2.dfy
@@ -0,0 +1,207 @@
+class IntList {

+  ghost var Repr: set<object>;

+  ghost var list: seq<int>;

+

+  var root: IntNode;

+

+  function Valid_repr(): bool

+    reads *;

+  {

+    this in Repr &&

+    null !in Repr &&

+    (root != null ==> root in Repr && root.Repr <= Repr && this !in root.Repr)

+  }

+

+  function Valid_self(): bool

+    reads *;

+  {

+    Valid_repr() &&

+    (root == null <==> |list| == 0) &&

+    (root != null ==> list == root.list)

+  }

+

+  function Valid(): bool

+    reads *;

+  {

+    this.Valid_self() &&

+    (root != null ==> root.Valid())

+  }

+

+  method Empty()

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures list == [];

+  {

+    this.list := [];

+    this.root := null;

+    // repr stuff

+    this.Repr := {this};

+  }

+

+  method SingletonTwo()

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures list == [2];

+  {

+    var gensym65 := new IntNode;

+    gensym65.data := 2;

+    gensym65.list := [2];

+    gensym65.next := null;

+    this.list := [2];

+    this.root := gensym65;

+    // repr stuff

+    gensym65.Repr := {gensym65};

+    this.Repr := {this} + this.root.Repr;

+  }

+

+  method OneTwo()

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures list == [1] + [2];

+  {

+    var gensym62 := new IntNode;

+    var gensym69 := new IntNode;

+    gensym62.data := 1;

+    gensym62.list := [1, 2];

+    gensym62.next := gensym69;

+    gensym69.data := 2;

+    gensym69.list := [2];

+    gensym69.next := null;

+    this.list := [1, 2];

+    this.root := gensym62;

+    // repr stuff

+    gensym69.Repr := {gensym69};

+    gensym62.Repr := {gensym62} + gensym62.next.Repr;

+    this.Repr := {this} + this.root.Repr;

+  }

+

+  method Singleton(p: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures list == [p];

+  {

+    var gensym66 := new IntNode;

+    gensym66.data := p;

+    gensym66.list := [p];

+    gensym66.next := null;

+    this.list := [p];

+    this.root := gensym66;

+    // repr stuff

+    gensym66.Repr := {gensym66};

+    this.Repr := {this} + this.root.Repr;

+  }

+

+  method TwoConsecutive(p: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures list == [p] + [p + 1];

+  {

+    var gensym63 := new IntNode;

+    var gensym71 := new IntNode;

+    gensym63.data := p;

+    gensym63.list := [p] + [p + 1];

+    gensym63.next := gensym71;

+    gensym71.data := p + 1;

+    gensym71.list := [p + 1];

+    gensym71.next := null;

+    this.list := [p] + [p + 1];

+    this.root := gensym63;

+    // repr stuff

+    gensym71.Repr := {gensym71};

+    gensym63.Repr := {gensym63} + gensym63.next.Repr;

+    this.Repr := {this} + this.root.Repr;

+  }

+

+  method Double(p: int, q: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures list == [p] + [q];

+  {

+    var gensym64 := new IntNode;

+    var gensym71 := new IntNode;

+    gensym64.data := p;

+    gensym64.list := [p] + [q];

+    gensym64.next := gensym71;

+    gensym71.data := q;

+    gensym71.list := [q];

+    gensym71.next := null;

+    this.list := [p] + [q];

+    this.root := gensym64;

+    // repr stuff

+    gensym71.Repr := {gensym71};

+    gensym64.Repr := {gensym64} + gensym64.next.Repr;

+    this.Repr := {this} + this.root.Repr;

+  }

+

+  method Sum(p: int, q: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures list == [p + q];

+  {

+    var gensym67 := new IntNode;

+    gensym67.data := p + q;

+    gensym67.list := [p + q];

+    gensym67.next := null;

+    this.list := [p + q];

+    this.root := gensym67;

+    // repr stuff

+    gensym67.Repr := {gensym67};

+    this.Repr := {this} + this.root.Repr;

+  }

+

+}

+

+class IntNode {

+  ghost var Repr: set<object>;

+  ghost var list: seq<int>;

+

+  var data: int;

+  var next: IntNode;

+

+  function Valid_repr(): bool

+    reads *;

+  {

+    this in Repr &&

+    null !in Repr &&

+    (next != null ==> next in Repr && next.Repr <= Repr && this !in next.Repr)

+  }

+

+  function Valid_self(): bool

+    reads *;

+  {

+    Valid_repr() &&

+    (next == null ==> list == [data] && list[0] == data) &&

+    (next != null ==> list == [data] + next.list) &&

+    (|list| > 0)

+  }

+

+  function Valid(): bool

+    reads *;

+  {

+    this.Valid_self() &&

+    (next != null ==> next.Valid_self() && (next.next != null ==> next.next.Valid_self()))

+  }

+

+  method SingletonZero()

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures list == [0];

+  {

+    this.data := 0;

+    this.list := [0];

+    this.next := null;

+    // repr stuff

+    this.Repr := {this};

+  }

+

+}

+

+

diff --git a/Source/Jennisys/examples/jennisys-synth_List3.dfy b/Source/Jennisys/examples/jennisys-synth_List3.dfy
new file mode 100644
index 00000000..e202412f
--- /dev/null
+++ b/Source/Jennisys/examples/jennisys-synth_List3.dfy
@@ -0,0 +1,255 @@
+class IntList {

+  ghost var Repr: set<object>;

+  ghost var list: seq<int>;

+

+  var root: IntNode;

+

+  function Valid_repr(): bool

+    reads *;

+  {

+    this in Repr &&

+    null !in Repr &&

+    (root != null ==> root in Repr && root.Repr <= Repr && this !in root.Repr)

+  }

+

+  function Valid_self(): bool

+    reads *;

+  {

+    Valid_repr() &&

+    (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 - 1] != null && list[i] == root.succ[i - 1].data)))

+  }

+

+  function Valid(): bool

+    reads *;

+  {

+    this.Valid_self() &&

+    (root != null ==> root.Valid())

+  }

+

+  method Empty()

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures list == [];

+  {

+    this.list := [];

+    this.root := null;

+    // repr stuff

+    this.Repr := {this};

+  }

+

+  method SingletonTwo()

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures list == [2];

+  {

+    var gensym65 := new IntNode;

+    gensym65.data := 2;

+    gensym65.next := null;

+    gensym65.succ := [];

+    this.list := [2];

+    this.root := gensym65;

+    // repr stuff

+    gensym65.Repr := {gensym65};

+    this.Repr := {this} + this.root.Repr;

+  }

+

+  method OneTwo()

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures list == [1] + [2];

+  {

+    var gensym63 := new IntNode;

+    var gensym75 := new IntNode;

+    gensym63.data := 1;

+    gensym63.next := gensym75;

+    gensym63.succ := [gensym75];

+    gensym75.data := 2;

+    gensym75.next := null;

+    gensym75.succ := [];

+    this.list := [1, 2];

+    this.root := gensym63;

+    // repr stuff

+    gensym75.Repr := {gensym75};

+    gensym63.Repr := {gensym63} + gensym63.next.Repr;

+    this.Repr := {this} + this.root.Repr;

+  }

+

+  method Singleton(p: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures list == [p];

+  {

+    var gensym66 := new IntNode;

+    gensym66.data := p;

+    gensym66.next := null;

+    gensym66.succ := [];

+    this.list := [p];

+    this.root := gensym66;

+    // repr stuff

+    gensym66.Repr := {gensym66};

+    this.Repr := {this} + this.root.Repr;

+  }

+

+  method TwoConsecutive(p: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures list == [p] + [p + 1];

+  {

+    var gensym64 := new IntNode;

+    var gensym75 := new IntNode;

+    gensym64.data := p;

+    gensym64.next := gensym75;

+    gensym64.succ := [gensym75];

+    gensym75.data := p + 1;

+    gensym75.next := null;

+    gensym75.succ := [];

+    this.list := [p] + [p + 1];

+    this.root := gensym64;

+    // repr stuff

+    gensym75.Repr := {gensym75};

+    gensym64.Repr := {gensym64} + gensym64.next.Repr;

+    this.Repr := {this} + this.root.Repr;

+  }

+

+  method Double(p: int, q: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures list == [p] + [q];

+  {

+    var gensym65 := new IntNode;

+    var gensym77 := new IntNode;

+    gensym65.data := p;

+    gensym65.next := gensym77;

+    gensym65.succ := [gensym77];

+    gensym77.data := q;

+    gensym77.next := null;

+    gensym77.succ := [];

+    this.list := [p] + [q];

+    this.root := gensym65;

+    // repr stuff

+    gensym77.Repr := {gensym77};

+    gensym65.Repr := {gensym65} + gensym65.next.Repr;

+    this.Repr := {this} + this.root.Repr;

+  }

+

+  method Sum(p: int, q: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures list == [p + q];

+  {

+    var gensym67 := new IntNode;

+    gensym67.data := p + q;

+    gensym67.next := null;

+    gensym67.succ := [];

+    this.list := [p + q];

+    this.root := gensym67;

+    // repr stuff

+    gensym67.Repr := {gensym67};

+    this.Repr := {this} + this.root.Repr;

+  }

+

+}

+

+class IntNode {

+  ghost var Repr: set<object>;

+  ghost var succ: seq<IntNode>;

+  ghost var data: int;

+

+  var next: IntNode;

+

+  function Valid_repr(): bool

+    reads *;

+  {

+    this in Repr &&

+    null !in Repr &&

+    (next != null ==> next in Repr && next.Repr <= Repr && this !in next.Repr)

+  }

+

+  function Valid_self(): bool

+    reads *;

+  {

+    Valid_repr() &&

+    (next == null ==> |succ| == 0) &&

+    (next != null ==> succ == [next] + next.succ) &&

+    (!(null in succ))

+  }

+

+  function Valid(): bool

+    reads *;

+  {

+    this.Valid_self() &&

+    (next != null ==> next.Valid_self() && (next.next != null ==> next.next.Valid_self()))

+  }

+

+  method Zero()

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures data == 0;

+    ensures succ == [];

+  {

+    this.data := 0;

+    this.next := null;

+    this.succ := [];

+    // repr stuff

+    this.Repr := {this};

+  }

+

+  method OneTwo()

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures data == 1;

+    ensures |succ| == 1;

+    ensures succ[0] != null;

+    ensures succ[0].data == 2;

+  {

+    var gensym71 := new IntNode;

+    gensym71.data := 2;

+    gensym71.next := null;

+    gensym71.succ := [];

+    this.data := 1;

+    this.next := gensym71;

+    this.succ := [gensym71];

+    // repr stuff

+    gensym71.Repr := {gensym71};

+    this.Repr := {this} + this.next.Repr;

+  }

+

+  method Init(p: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures data == p;

+  {

+    this.data := p;

+    this.next := null;

+    this.succ := [];

+    // repr stuff

+    this.Repr := {this};

+  }

+

+  method InitInc(p: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures data == p + 1;

+  {

+    this.data := p + 1;

+    this.next := null;

+    this.succ := [];

+    // repr stuff

+    this.Repr := {this};

+  }

+

+}

+

+

diff --git a/Source/Jennisys/examples/jennisys-synth_Number.dfy b/Source/Jennisys/examples/jennisys-synth_Number.dfy
new file mode 100644
index 00000000..5ede7f5c
--- /dev/null
+++ b/Source/Jennisys/examples/jennisys-synth_Number.dfy
@@ -0,0 +1,202 @@
+class Number {

+  ghost var Repr: set<object>;

+  ghost var num: int;

+

+

+  function Valid_repr(): bool

+    reads *;

+  {

+    this in Repr &&

+    null !in Repr

+  }

+

+  function Valid_self(): bool

+    reads *;

+  {

+    Valid_repr() &&

+    true

+  }

+

+  function Valid(): bool

+    reads *;

+  {

+    this.Valid_self() &&

+    true

+  }

+

+  method Init(p: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures num == p;

+  {

+    this.num := p;

+    // repr stuff

+    this.Repr := {this};

+  }

+

+  method Double(p: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures num == 2 * p;

+  {

+    this.num := 2 * p;

+    // repr stuff

+    this.Repr := {this};

+  }

+

+  method Sum(a: int, b: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures num == a + b;

+  {

+    this.num := a + b;

+    // repr stuff

+    this.Repr := {this};

+  }

+

+  method Min2(a: int, b: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures a < b ==> num == a;

+    ensures a >= b ==> num == b;

+  {

+    if (a >= b ==> a == b) {

+      this.num := a;

+      // repr stuff

+      this.Repr := {this};

+    } else {

+      this.num := b;

+      // repr stuff

+      this.Repr := {this};

+    }

+  }

+

+  method Min22(a: int, b: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures num in {a, b};

+    ensures num <= a;

+    ensures num <= b;

+  {

+    if (a <= b) {

+      this.num := a;

+      // repr stuff

+      this.Repr := {this};

+    } else {

+      this.num := b;

+      // repr stuff

+      this.Repr := {this};

+    }

+  }

+

+  method Min3(a: int, b: int, c: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures num in {a, b, c};

+    ensures num <= a;

+    ensures num <= b;

+    ensures num <= c;

+  {

+    if (a <= b && a <= c) {

+      this.num := a;

+      // repr stuff

+      this.Repr := {this};

+    } else {

+      if (c <= a && c <= b) {

+        this.num := c;

+        // repr stuff

+        this.Repr := {this};

+      } else {

+        this.num := b;

+        // repr stuff

+        this.Repr := {this};

+      }

+    }

+  }

+

+  method MinSum(a: int, b: int, c: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures num in {a + b, a + c, b + c};

+    ensures num <= a + b;

+    ensures num <= b + c;

+    ensures num <= a + c;

+  {

+    if (a + b <= b + c && a + b <= a + c) {

+      this.num := a + b;

+      // repr stuff

+      this.Repr := {this};

+    } else {

+      if (a + c <= a + b && a + c <= b + c) {

+        this.num := a + c;

+        // repr stuff

+        this.Repr := {this};

+      } else {

+        this.num := b + c;

+        // repr stuff

+        this.Repr := {this};

+      }

+    }

+  }

+

+  method Min4(a: int, b: int, c: int, d: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures num in {a, b, c, d};

+    ensures num <= a;

+    ensures num <= b;

+    ensures num <= c;

+    ensures num <= d;

+  {

+    if (a <= b && (a <= c && a <= d)) {

+      this.num := a;

+      // repr stuff

+      this.Repr := {this};

+    } else {

+      if (d <= a && (d <= b && d <= c)) {

+        this.num := d;

+        // repr stuff

+        this.Repr := {this};

+      } else {

+        if (c <= a && (c <= b && c <= d)) {

+          this.num := c;

+          // repr stuff

+          this.Repr := {this};

+        } else {

+          this.num := b;

+          // repr stuff

+          this.Repr := {this};

+        }

+      }

+    }

+  }

+

+  method Abs(a: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures a < 0 ==> num == -a;

+    ensures a >= 0 ==> num == a;

+  {

+    if (!(a >= 0)) {

+      this.num := -a;

+      // repr stuff

+      this.Repr := {this};

+    } else {

+      this.num := a;

+      // repr stuff

+      this.Repr := {this};

+    }

+  }

+

+}

+

+

diff --git a/Source/Jennisys/examples/jennisys-synth_Set.dfy b/Source/Jennisys/examples/jennisys-synth_Set.dfy
new file mode 100644
index 00000000..efc9aa07
--- /dev/null
+++ b/Source/Jennisys/examples/jennisys-synth_Set.dfy
@@ -0,0 +1,344 @@
+class Set {

+  ghost var Repr: set<object>;

+  ghost var elems: set<int>;

+

+  var root: SetNode;

+

+  function Valid_repr(): bool

+    reads *;

+  {

+    this in Repr &&

+    null !in Repr &&

+    (root != null ==> root in Repr && root.Repr <= Repr && this !in root.Repr)

+  }

+

+  function Valid_self(): bool

+    reads *;

+  {

+    Valid_repr() &&

+    (root == null ==> elems == {}) &&

+    (root != null ==> elems == root.elems)

+  }

+

+  function Valid(): bool

+    reads *;

+  {

+    this.Valid_self() &&

+    (root != null ==> root.Valid())

+  }

+

+  method Empty()

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures elems == {};

+  {

+    this.elems := {};

+    this.root := null;

+    // repr stuff

+    this.Repr := {this};

+  }

+

+  method Singleton(t: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures elems == {t};

+  {

+    var gensym66 := new SetNode;

+    gensym66.data := t;

+    gensym66.elems := {t};

+    gensym66.left := null;

+    gensym66.right := null;

+    this.elems := {t};

+    this.root := gensym66;

+    // repr stuff

+    gensym66.Repr := {gensym66};

+    this.Repr := {this} + this.root.Repr;

+  }

+

+  method Sum(p: int, q: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures elems == {p + q};

+  {

+    var gensym68 := new SetNode;

+    gensym68.data := p + q;

+    gensym68.elems := {p + q};

+    gensym68.left := null;

+    gensym68.right := null;

+    this.elems := {p + q};

+    this.root := gensym68;

+    // repr stuff

+    gensym68.Repr := {gensym68};

+    this.Repr := {this} + this.root.Repr;

+  }

+

+  method Double(p: int, q: int)

+    modifies this;

+    requires p != q;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures elems == {p, q};

+  {

+    if (q < p) {

+      var gensym71 := new SetNode;

+      var gensym75 := new SetNode;

+      gensym71.data := p;

+      gensym71.elems := {p, q};

+      gensym71.left := gensym75;

+      gensym71.right := null;

+      gensym75.data := q;

+      gensym75.elems := {q};

+      gensym75.left := null;

+      gensym75.right := null;

+      this.elems := {p, q};

+      this.root := gensym71;

+      // repr stuff

+      gensym75.Repr := {gensym75};

+      gensym71.Repr := {gensym71} + gensym71.left.Repr;

+      this.Repr := {this} + this.root.Repr;

+    } else {

+      var gensym71 := new SetNode;

+      var gensym75 := new SetNode;

+      gensym71.data := q;

+      gensym71.elems := {p, q};

+      gensym71.left := gensym75;

+      gensym71.right := null;

+      gensym75.data := p;

+      gensym75.elems := {p};

+      gensym75.left := null;

+      gensym75.right := null;

+      this.elems := {p, q};

+      this.root := gensym71;

+      // repr stuff

+      gensym75.Repr := {gensym75};

+      gensym71.Repr := {gensym71} + gensym71.left.Repr;

+      this.Repr := {this} + this.root.Repr;

+    }

+  }

+

+}

+

+class SetNode {

+  ghost var Repr: set<object>;

+  ghost var elems: set<int>;

+

+  var data: int;

+  var left: SetNode;

+  var right: SetNode;

+

+  function Valid_repr(): bool

+    reads *;

+  {

+    this in Repr &&

+    null !in Repr &&

+    (left != null ==> left in Repr && left.Repr <= Repr && this !in left.Repr) &&

+    (right != null ==> right in Repr && right.Repr <= Repr && this !in right.Repr)

+  }

+

+  function Valid_self(): bool

+    reads *;

+  {

+    Valid_repr() &&

+    (elems == ({data} + (if left != null then left.elems else {})) + (if right != null then right.elems else {})) &&

+    (left != null ==> (forall e :: e in left.elems ==> e < data)) &&

+    (right != null ==> (forall e :: e in right.elems ==> e > data))

+  }

+

+  function Valid(): bool

+    reads *;

+  {

+    this.Valid_self() &&

+    (left != null ==> left.Valid_self() && (left.left != null ==> left.left.Valid_self())) &&

+    (right != null ==> right.Valid_self() && (right.right != null ==> right.right.Valid_self()))

+  }

+

+  method Init(t: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures elems == {t};

+  {

+    this.data := t;

+    this.elems := {t};

+    this.left := null;

+    this.right := null;

+    // repr stuff

+    this.Repr := {this};

+  }

+

+  method Double(p: int, q: int)

+    modifies this;

+    requires p != q;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures elems == {p, q};

+  {

+    if (q > p) {

+      var gensym79 := new SetNode;

+      gensym79.data := q;

+      gensym79.elems := {q};

+      gensym79.left := null;

+      gensym79.right := null;

+      this.data := p;

+      this.elems := {p, q};

+      this.left := null;

+      this.right := gensym79;

+      // repr stuff

+      gensym79.Repr := {gensym79};

+      this.Repr := {this} + this.right.Repr;

+    } else {

+      var gensym79 := new SetNode;

+      gensym79.data := p;

+      gensym79.elems := {p};

+      gensym79.left := null;

+      gensym79.right := null;

+      this.data := q;

+      this.elems := {p, q};

+      this.left := null;

+      this.right := gensym79;

+      // repr stuff

+      gensym79.Repr := {gensym79};

+      this.Repr := {this} + this.right.Repr;

+    }

+  }

+

+  method Triple(p: int, q: int, r: int)

+    modifies this;

+    requires p != q;

+    requires q != r;

+    requires r != p;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures elems == {p, q, r};

+  {

+    if (p < q && r > q) {

+      var gensym83 := new SetNode;

+      var gensym84 := new SetNode;

+      gensym83.data := r;

+      gensym83.elems := {r};

+      gensym83.left := null;

+      gensym83.right := null;

+      gensym84.data := p;

+      gensym84.elems := {p};

+      gensym84.left := null;

+      gensym84.right := null;

+      this.data := q;

+      this.elems := {p, q, r};

+      this.left := gensym84;

+      this.right := gensym83;

+      // repr stuff

+      gensym83.Repr := {gensym83};

+      gensym84.Repr := {gensym84};

+      this.Repr := ({this} + this.left.Repr) + this.right.Repr;

+    } else {

+      if (p < r && q > r) {

+        var gensym85 := new SetNode;

+        var gensym86 := new SetNode;

+        gensym85.data := q;

+        gensym85.elems := {q};

+        gensym85.left := null;

+        gensym85.right := null;

+        gensym86.data := p;

+        gensym86.elems := {p};

+        gensym86.left := null;

+        gensym86.right := null;

+        this.data := r;

+        this.elems := {p, q, r};

+        this.left := gensym86;

+        this.right := gensym85;

+        // repr stuff

+        gensym85.Repr := {gensym85};

+        gensym86.Repr := {gensym86};

+        this.Repr := ({this} + this.left.Repr) + this.right.Repr;

+      } else {

+        if (r < p && q > p) {

+          var gensym84 := new SetNode;

+          var gensym85 := new SetNode;

+          gensym84.data := q;

+          gensym84.elems := {q};

+          gensym84.left := null;

+          gensym84.right := null;

+          gensym85.data := r;

+          gensym85.elems := {r};

+          gensym85.left := null;

+          gensym85.right := null;

+          this.data := p;

+          this.elems := {p, q, r};

+          this.left := gensym85;

+          this.right := gensym84;

+          // repr stuff

+          gensym84.Repr := {gensym84};

+          gensym85.Repr := {gensym85};

+          this.Repr := ({this} + this.left.Repr) + this.right.Repr;

+        } else {

+          if (q < p && r > p) {

+            var gensym82 := new SetNode;

+            var gensym83 := new SetNode;

+            gensym82.data := r;

+            gensym82.elems := {r};

+            gensym82.left := null;

+            gensym82.right := null;

+            gensym83.data := q;

+            gensym83.elems := {q};

+            gensym83.left := null;

+            gensym83.right := null;

+            this.data := p;

+            this.elems := {p, q, r};

+            this.left := gensym83;

+            this.right := gensym82;

+            // repr stuff

+            gensym82.Repr := {gensym82};

+            gensym83.Repr := {gensym83};

+            this.Repr := ({this} + this.left.Repr) + this.right.Repr;

+          } else {

+            if (q < r && p > r) {

+              var gensym85 := new SetNode;

+              var gensym86 := new SetNode;

+              gensym85.data := p;

+              gensym85.elems := {p};

+              gensym85.left := null;

+              gensym85.right := null;

+              gensym86.data := q;

+              gensym86.elems := {q};

+              gensym86.left := null;

+              gensym86.right := null;

+              this.data := r;

+              this.elems := {p, q, r};

+              this.left := gensym86;

+              this.right := gensym85;

+              // repr stuff

+              gensym85.Repr := {gensym85};

+              gensym86.Repr := {gensym86};

+              this.Repr := ({this} + this.left.Repr) + this.right.Repr;

+            } else {

+              var gensym82 := new SetNode;

+              var gensym83 := new SetNode;

+              gensym82.data := p;

+              gensym82.elems := {p};

+              gensym82.left := null;

+              gensym82.right := null;

+              gensym83.data := r;

+              gensym83.elems := {r};

+              gensym83.left := null;

+              gensym83.right := null;

+              this.data := q;

+              this.elems := {p, q, r};

+              this.left := gensym83;

+              this.right := gensym82;

+              // repr stuff

+              gensym82.Repr := {gensym82};

+              gensym83.Repr := {gensym83};

+              this.Repr := ({this} + this.left.Repr) + this.right.Repr;

+            }

+          }

+        }

+      }

+    }

+  }

+

+}

+

+

diff --git a/Source/Jennisys/examples/mod/jennisys-synth_List.dfy b/Source/Jennisys/examples/mod/jennisys-synth_List.dfy
new file mode 100644
index 00000000..474eb9f1
--- /dev/null
+++ b/Source/Jennisys/examples/mod/jennisys-synth_List.dfy
@@ -0,0 +1,202 @@
+class List<T> {

+  ghost var Repr: set<object>;

+  ghost var list: seq<T>;

+

+  var root: Node<T>;

+

+  function Valid_repr(): bool

+    reads *;

+  {

+    this in Repr &&

+    null !in Repr &&

+    (root != null ==> root in Repr && root.Repr <= Repr && this !in root.Repr)

+  }

+

+  function Valid_self(): bool

+    reads *;

+  {

+    Valid_repr() &&

+    (root == null ==> |list| == 0) &&

+    (root != null ==> list == root.list)

+  }

+

+  function Valid(): bool

+    reads *;

+  {

+    this.Valid_self() &&

+    (root != null ==> root.Valid())

+  }

+

+

+  method Double(p: T, q: T)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures list == [p, q];

+  {

+    var gensym68 := new Node<T>;

+    gensym68._synth_List_Double_gensym68(p, q);

+    this.list := [p, q];

+    this.root := gensym68;

+    // repr stuff

+    this.Repr := {this} + this.root.Repr;

+  }

+

+

+  method Empty()

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures list == [];

+  {

+    this.list := [];

+    this.root := null;

+    // repr stuff

+    this.Repr := {this};

+  }

+

+

+  method Singleton(t: T)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures list == [t];

+  {

+    var gensym69 := new Node<T>;

+    gensym69._synth_List_Singleton_gensym69(t);

+    this.list := [t];

+    this.root := gensym69;

+    // repr stuff

+    this.Repr := {this} + this.root.Repr;

+  }

+

+}

+

+class Node<T> {

+  ghost var Repr: set<object>;

+  ghost var list: seq<T>;

+

+  var data: T;

+  var next: Node<T>;

+

+  function Valid_repr(): bool

+    reads *;

+  {

+    this in Repr &&

+    null !in Repr &&

+    (next != null ==> next in Repr && next.Repr <= Repr && this !in next.Repr)

+  }

+

+  function Valid_self(): bool

+    reads *;

+  {

+    Valid_repr() &&

+    (next == null <==> list == [data] && list[0] == data) &&

+    (next != null ==> list == [data] + next.list) &&

+    (|list| > 0)

+  }

+

+  function Valid(): bool

+    reads *;

+  {

+    this.Valid_self() &&

+    (next != null ==> next.Valid_self()) &&

+    (next != null && next.next != null ==> next.next.Valid_self())

+  }

+

+

+  method Init(t: T)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures list == [t];

+  {

+    this.data := t;

+    this.list := [t];

+    this.next := null;

+    // repr stuff

+    this.Repr := {this};

+  }

+

+

+  method _synth_List_Double_gensym68(p: T, q: T)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures |list| == 2;

+    ensures list[0] == p;

+    ensures list[1] == q;

+  {

+    var gensym75 := new Node<T>;

+    gensym75._synth_Node__synth_List_Double_gensym68_gensym75(q);

+    this.data := p;

+    this.list := [p, q];

+    this.next := gensym75;

+    // repr stuff

+    this.Repr := {this} + this.next.Repr;

+  }

+

+

+  method _synth_List_Singleton_gensym69(t: T)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures |list| == 1;

+    ensures list[0] == t;

+  {

+    this.data := t;

+    this.list := [t];

+    this.next := null;

+    // repr stuff

+    this.Repr := {this};

+  }

+

+

+  method Double(p: T, q: T)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures list == [p, q];

+  {

+    var gensym73 := new Node<T>;

+    gensym73._synth_Node_Double_gensym73(q);

+    this.data := p;

+    this.list := [p, q];

+    this.next := gensym73;

+    // repr stuff

+    this.Repr := {this} + this.next.Repr;

+  }

+

+

+  method _synth_Node_Double_gensym73(q: T)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures |list| == 1;

+    ensures list[0] == q;

+  {

+    this.data := q;

+    this.list := [q];

+    this.next := null;

+    // repr stuff

+    this.Repr := {this};

+  }

+

+

+  method _synth_Node__synth_List_Double_gensym68_gensym75(q: T)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures |list| == 1;

+    ensures list[0] == q;

+  {

+    this.data := q;

+    this.list := [q];

+    this.next := null;

+    // repr stuff

+    this.Repr := {this};

+  }

+

+}

+

+

diff --git a/Source/Jennisys/examples/mod/jennisys-synth_List2.dfy b/Source/Jennisys/examples/mod/jennisys-synth_List2.dfy
new file mode 100644
index 00000000..46213b46
--- /dev/null
+++ b/Source/Jennisys/examples/mod/jennisys-synth_List2.dfy
@@ -0,0 +1,323 @@
+class IntList {

+  ghost var Repr: set<object>;

+  ghost var list: seq<int>;

+

+  var root: IntNode;

+

+  function Valid_repr(): bool

+    reads *;

+  {

+    this in Repr &&

+    null !in Repr &&

+    (root != null ==> root in Repr && root.Repr <= Repr && this !in root.Repr)

+  }

+

+  function Valid_self(): bool

+    reads *;

+  {

+    Valid_repr() &&

+    (root == null <==> |list| == 0) &&

+    (root != null ==> list == root.list)

+  }

+

+  function Valid(): bool

+    reads *;

+  {

+    this.Valid_self() &&

+    (root != null ==> root.Valid())

+  }

+

+

+  method Double(p: int, q: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures list == [p] + [q];

+  {

+    var gensym67 := new IntNode;

+    gensym67._synth_IntList_Double_gensym67(p, q);

+    this.list := [p] + [q];

+    this.root := gensym67;

+    // repr stuff

+    this.Repr := {this} + this.root.Repr;

+  }

+

+

+  method Empty()

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures list == [];

+  {

+    this.list := [];

+    this.root := null;

+    // repr stuff

+    this.Repr := {this};

+  }

+

+

+  method OneTwo()

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures list == [1, 2];

+  {

+    var gensym65 := new IntNode;

+    gensym65._synth_IntList_OneTwo_gensym65();

+    this.list := [1, 2];

+    this.root := gensym65;

+    // repr stuff

+    this.Repr := {this} + this.root.Repr;

+  }

+

+

+  method Singleton(p: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures list == [p];

+  {

+    var gensym70 := new IntNode;

+    gensym70._synth_IntList_Singleton_gensym70(p);

+    this.list := [p];

+    this.root := gensym70;

+    // repr stuff

+    this.Repr := {this} + this.root.Repr;

+  }

+

+

+  method SingletonTwo()

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures list == [2];

+  {

+    var gensym69 := new IntNode;

+    gensym69._synth_IntList_SingletonTwo_gensym69();

+    this.list := [2];

+    this.root := gensym69;

+    // repr stuff

+    this.Repr := {this} + this.root.Repr;

+  }

+

+

+  method Sum(p: int, q: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures list == [p + q];

+  {

+    var gensym71 := new IntNode;

+    gensym71._synth_IntList_Sum_gensym71(p, q);

+    this.list := [p + q];

+    this.root := gensym71;

+    // repr stuff

+    this.Repr := {this} + this.root.Repr;

+  }

+

+

+  method TwoConsecutive(p: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures list == [p] + [p + 1];

+  {

+    var gensym66 := new IntNode;

+    gensym66._synth_IntList_TwoConsecutive_gensym66(p);

+    this.list := [p] + [p + 1];

+    this.root := gensym66;

+    // repr stuff

+    this.Repr := {this} + this.root.Repr;

+  }

+

+}

+

+class IntNode {

+  ghost var Repr: set<object>;

+  ghost var list: seq<int>;

+

+  var data: int;

+  var next: IntNode;

+

+  function Valid_repr(): bool

+    reads *;

+  {

+    this in Repr &&

+    null !in Repr &&

+    (next != null ==> next in Repr && next.Repr <= Repr && this !in next.Repr)

+  }

+

+  function Valid_self(): bool

+    reads *;

+  {

+    Valid_repr() &&

+    (next == null ==> list == [data] && list[0] == data) &&

+    (next != null ==> list == [data] + next.list) &&

+    (|list| > 0)

+  }

+

+  function Valid(): bool

+    reads *;

+  {

+    this.Valid_self() &&

+    (next != null ==> next.Valid_self()) &&

+    (next != null && next.next != null ==> next.next.Valid_self())

+  }

+

+

+  method SingletonZero()

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures list == [0];

+  {

+    this.data := 0;

+    this.list := [0];

+    this.next := null;

+    // repr stuff

+    this.Repr := {this};

+  }

+

+

+  method _synth_IntList_Double_gensym67(p: int, q: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures list == [p] + [q];

+  {

+    var gensym78 := new IntNode;

+    gensym78._synth_IntNode__synth_IntList_Double_gensym67_gensym78(q);

+    this.data := p;

+    this.list := [p] + [q];

+    this.next := gensym78;

+    // repr stuff

+    this.Repr := {this} + this.next.Repr;

+  }

+

+

+  method _synth_IntList_OneTwo_gensym65()

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures |list| == 2;

+    ensures list[0] == 1;

+    ensures list[1] == 2;

+  {

+    var gensym75 := new IntNode;

+    gensym75._synth_IntNode__synth_IntList_OneTwo_gensym65_gensym75();

+    this.data := 1;

+    this.list := [1, 2];

+    this.next := gensym75;

+    // repr stuff

+    this.Repr := {this} + this.next.Repr;

+  }

+

+

+  method _synth_IntList_SingletonTwo_gensym69()

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures |list| == 1;

+    ensures list[0] == 2;

+  {

+    this.data := 2;

+    this.list := [2];

+    this.next := null;

+    // repr stuff

+    this.Repr := {this};

+  }

+

+

+  method _synth_IntList_Singleton_gensym70(p: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures |list| == 1;

+    ensures list[0] == p;

+  {

+    this.data := p;

+    this.list := [p];

+    this.next := null;

+    // repr stuff

+    this.Repr := {this};

+  }

+

+

+  method _synth_IntList_Sum_gensym71(p: int, q: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures |list| == 1;

+    ensures list[0] == p + q;

+  {

+    this.data := p + q;

+    this.list := [p + q];

+    this.next := null;

+    // repr stuff

+    this.Repr := {this};

+  }

+

+

+  method _synth_IntList_TwoConsecutive_gensym66(p: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures list == [p] + [p + 1];

+  {

+    var gensym78 := new IntNode;

+    gensym78._synth_IntNode__synth_IntList_TwoConsecutive_gensym66_gensym78(p);

+    this.data := p;

+    this.list := [p] + [p + 1];

+    this.next := gensym78;

+    // repr stuff

+    this.Repr := {this} + this.next.Repr;

+  }

+

+

+  method _synth_IntNode__synth_IntList_Double_gensym67_gensym78(q: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures |list| == 1;

+    ensures list[0] == q;

+  {

+    this.data := q;

+    this.list := [q];

+    this.next := null;

+    // repr stuff

+    this.Repr := {this};

+  }

+

+

+  method _synth_IntNode__synth_IntList_OneTwo_gensym65_gensym75()

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures |list| == 1;

+    ensures list[0] == 2;

+  {

+    this.data := 2;

+    this.list := [2];

+    this.next := null;

+    // repr stuff

+    this.Repr := {this};

+  }

+

+

+  method _synth_IntNode__synth_IntList_TwoConsecutive_gensym66_gensym78(p: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures |list| == 1;

+    ensures list[0] == p + 1;

+  {

+    this.data := p + 1;

+    this.list := [p + 1];

+    this.next := null;

+    // repr stuff

+    this.Repr := {this};

+  }

+

+}

+

+

diff --git a/Source/Jennisys/examples/mod/jennisys-synth_List3.dfy b/Source/Jennisys/examples/mod/jennisys-synth_List3.dfy
new file mode 100644
index 00000000..e079b608
--- /dev/null
+++ b/Source/Jennisys/examples/mod/jennisys-synth_List3.dfy
@@ -0,0 +1,393 @@
+class IntList {

+  ghost var Repr: set<object>;

+  ghost var list: seq<int>;

+

+  var root: IntNode;

+

+  function Valid_repr(): bool

+    reads *;

+  {

+    this in Repr &&

+    null !in Repr &&

+    (root != null ==> root in Repr && root.Repr <= Repr && this !in root.Repr)

+  }

+

+  function Valid_self(): bool

+    reads *;

+  {

+    Valid_repr() &&

+    (root == null ==> |list| == 0) &&

+    (root != null ==> |list| == |root.succ| + 1 && (list[0] == root.data && (forall i :: 1 <= i && i <= |root.succ| ==> root.succ[i - 1] != null && list[i] == root.succ[i - 1].data)))

+  }

+

+  function Valid(): bool

+    reads *;

+  {

+    this.Valid_self() &&

+    (root != null ==> root.Valid())

+  }

+

+

+  method Double(p: int, q: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures list == [p] + [q];

+  {

+    var gensym68 := new IntNode;

+    gensym68._synth_IntList_Double_gensym68(p, q);

+    this.list := [p] + [q];

+    this.root := gensym68;

+    // repr stuff

+    this.Repr := {this} + this.root.Repr;

+  }

+

+

+  method Empty()

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures list == [];

+  {

+    this.list := [];

+    this.root := null;

+    // repr stuff

+    this.Repr := {this};

+  }

+

+

+  method OneTwo()

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures list == [1, 2];

+  {

+    var gensym65 := new IntNode;

+    gensym65._synth_IntList_OneTwo_gensym65();

+    this.list := [1, 2];

+    this.root := gensym65;

+    // repr stuff

+    this.Repr := {this} + this.root.Repr;

+  }

+

+

+  method Singleton(p: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures list == [p];

+  {

+    var gensym70 := new IntNode;

+    gensym70._synth_IntList_Singleton_gensym70(p);

+    this.list := [p];

+    this.root := gensym70;

+    // repr stuff

+    this.Repr := {this} + this.root.Repr;

+  }

+

+

+  method SingletonTwo()

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures list == [2];

+  {

+    var gensym69 := new IntNode;

+    gensym69._synth_IntList_SingletonTwo_gensym69();

+    this.list := [2];

+    this.root := gensym69;

+    // repr stuff

+    this.Repr := {this} + this.root.Repr;

+  }

+

+

+  method Sum(p: int, q: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures list == [p + q];

+  {

+    var gensym71 := new IntNode;

+    gensym71._synth_IntList_Sum_gensym71(p, q);

+    this.list := [p + q];

+    this.root := gensym71;

+    // repr stuff

+    this.Repr := {this} + this.root.Repr;

+  }

+

+

+  method TwoConsecutive(p: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures list == [p] + [p + 1];

+  {

+    var gensym67 := new IntNode;

+    gensym67._synth_IntList_TwoConsecutive_gensym67(p);

+    this.list := [p] + [p + 1];

+    this.root := gensym67;

+    // repr stuff

+    this.Repr := {this} + this.root.Repr;

+  }

+

+}

+

+class IntNode {

+  ghost var Repr: set<object>;

+  ghost var succ: seq<IntNode>;

+  ghost var data: int;

+

+  var next: IntNode;

+

+  function Valid_repr(): bool

+    reads *;

+  {

+    this in Repr &&

+    null !in Repr &&

+    (next != null ==> next in Repr && next.Repr <= Repr && this !in next.Repr)

+  }

+

+  function Valid_self(): bool

+    reads *;

+  {

+    Valid_repr() &&

+    (next == null ==> |succ| == 0) &&

+    (next != null ==> succ == [next] + next.succ) &&

+    (!(null in succ))

+  }

+

+  function Valid(): bool

+    reads *;

+  {

+    this.Valid_self() &&

+    (next != null ==> next.Valid_self()) &&

+    (next != null && next.next != null ==> next.next.Valid_self())

+  }

+

+

+  method Init(p: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures data == p;

+  {

+    this.data := p;

+    this.next := null;

+    this.succ := [];

+    // repr stuff

+    this.Repr := {this};

+  }

+

+

+  method InitInc(p: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures data == p + 1;

+  {

+    this.data := p + 1;

+    this.next := null;

+    this.succ := [];

+    // repr stuff

+    this.Repr := {this};

+  }

+

+

+  method Zero()

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures data == 0;

+    ensures succ == [];

+  {

+    this.data := 0;

+    this.next := null;

+    this.succ := [];

+    // repr stuff

+    this.Repr := {this};

+  }

+

+

+  method _synth_IntList_Double_gensym68(p: int, q: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures data == p;

+    ensures |succ| == 1;

+    ensures succ[0].data == q;

+    ensures succ[0].succ == [];

+  {

+    var gensym80 := new IntNode;

+    gensym80._synth_IntNode__synth_IntList_Double_gensym68_gensym80(q);

+    this.data := p;

+    this.next := gensym80;

+    this.succ := [gensym80];

+    // repr stuff

+    this.Repr := {this} + this.next.Repr;

+  }

+

+

+  method _synth_IntList_OneTwo_gensym65()

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures data == 1;

+    ensures |succ| == 1;

+    ensures succ[0].data == 2;

+    ensures succ[0].succ == [];

+  {

+    var gensym78 := new IntNode;

+    gensym78._synth_IntNode__synth_IntList_OneTwo_gensym65_gensym78();

+    this.data := 1;

+    this.next := gensym78;

+    this.succ := [gensym78];

+    // repr stuff

+    this.Repr := {this} + this.next.Repr;

+  }

+

+

+  method _synth_IntList_SingletonTwo_gensym69()

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures data == 2;

+    ensures |succ| == 0;

+  {

+    this.data := 2;

+    this.next := null;

+    this.succ := [];

+    // repr stuff

+    this.Repr := {this};

+  }

+

+

+  method _synth_IntList_Singleton_gensym70(p: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures data == p;

+    ensures |succ| == 0;

+  {

+    this.data := p;

+    this.next := null;

+    this.succ := [];

+    // repr stuff

+    this.Repr := {this};

+  }

+

+

+  method _synth_IntList_Sum_gensym71(p: int, q: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures data == p + q;

+    ensures |succ| == 0;

+  {

+    this.data := p + q;

+    this.next := null;

+    this.succ := [];

+    // repr stuff

+    this.Repr := {this};

+  }

+

+

+  method _synth_IntList_TwoConsecutive_gensym67(p: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures data == p;

+    ensures |succ| == 1;

+    ensures succ[0].data == p + 1;

+    ensures succ[0].succ == [];

+  {

+    var gensym79 := new IntNode;

+    gensym79._synth_IntNode__synth_IntList_TwoConsecutive_gensym67_gensym79(p);

+    this.data := p;

+    this.next := gensym79;

+    this.succ := [gensym79];

+    // repr stuff

+    this.Repr := {this} + this.next.Repr;

+  }

+

+

+  method OneTwo()

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures data == 1;

+    ensures |succ| == 1;

+    ensures succ[0] != null;

+    ensures succ[0].data == 2;

+  {

+    var gensym73 := new IntNode;

+    gensym73._synth_IntNode_OneTwo_gensym73();

+    this.data := 1;

+    this.next := gensym73;

+    this.succ := [gensym73];

+    // repr stuff

+    this.Repr := {this} + this.next.Repr;

+  }

+

+

+  method _synth_IntNode_OneTwo_gensym73()

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures data == 2;

+    ensures |succ| == 0;

+  {

+    this.data := 2;

+    this.next := null;

+    this.succ := [];

+    // repr stuff

+    this.Repr := {this};

+  }

+

+

+  method _synth_IntNode__synth_IntList_Double_gensym68_gensym80(q: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures data == q;

+    ensures |succ| == 0;

+  {

+    this.data := q;

+    this.next := null;

+    this.succ := [];

+    // repr stuff

+    this.Repr := {this};

+  }

+

+

+  method _synth_IntNode__synth_IntList_OneTwo_gensym65_gensym78()

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures data == 2;

+    ensures |succ| == 0;

+  {

+    this.data := 2;

+    this.next := null;

+    this.succ := [];

+    // repr stuff

+    this.Repr := {this};

+  }

+

+

+  method _synth_IntNode__synth_IntList_TwoConsecutive_gensym67_gensym79(p: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures data == p + 1;

+    ensures |succ| == 0;

+  {

+    this.data := p + 1;

+    this.next := null;

+    this.succ := [];

+    // repr stuff

+    this.Repr := {this};

+  }

+

+}

+

+

diff --git a/Source/Jennisys/examples/mod/jennisys-synth_Number.dfy b/Source/Jennisys/examples/mod/jennisys-synth_Number.dfy
new file mode 100644
index 00000000..3f1e6b4b
--- /dev/null
+++ b/Source/Jennisys/examples/mod/jennisys-synth_Number.dfy
@@ -0,0 +1,233 @@
+class Number {

+  ghost var Repr: set<object>;

+  ghost var num: int;

+

+

+  function Valid_repr(): bool

+    reads *;

+  {

+    this in Repr &&

+    null !in Repr

+  }

+

+  function Valid_self(): bool

+    reads *;

+  {

+    Valid_repr() &&

+    true

+  }

+

+  function Valid(): bool

+    reads *;

+  {

+    this.Valid_self() &&

+    true

+  }

+

+

+  method Double(p: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures num == 2 * p;

+  {

+    this.num := 2 * p;

+    // repr stuff

+    this.Repr := {this};

+  }

+

+

+  method Init(p: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures num == p;

+  {

+    this.num := p;

+    // repr stuff

+    this.Repr := {this};

+  }

+

+

+  method Sum(a: int, b: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures num == a + b;

+  {

+    this.num := a + b;

+    // repr stuff

+    this.Repr := {this};

+  }

+

+

+  method Abs(a: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures num in {a, -a};

+    ensures num >= 0;

+  {

+    if (a >= 0) {

+      this.num := a;

+      // repr stuff

+      this.Repr := {this};

+    } else {

+      this.num := -a;

+      // repr stuff

+      this.Repr := {this};

+    }

+  }

+

+

+  method Min4(a: int, b: int, c: int, d: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures num in {a, b, c, d};

+    ensures (forall x :: x in {a, b, c, d} ==> num <= x);

+  {

+    if (a <= b && (a <= c && a <= d)) {

+      this.num := a;

+      // repr stuff

+      this.Repr := {this};

+    } else {

+      if (d <= a && (d <= b && d <= c)) {

+        this.num := d;

+        // repr stuff

+        this.Repr := {this};

+      } else {

+        if (c <= a && (c <= b && c <= d)) {

+          this.num := c;

+          // repr stuff

+          this.Repr := {this};

+        } else {

+          this.num := b;

+          // repr stuff

+          this.Repr := {this};

+        }

+      }

+    }

+  }

+

+

+  method MinSum(a: int, b: int, c: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures num in {a + b, a + c, b + c};

+    ensures num <= a + b;

+    ensures num <= b + c;

+    ensures num <= a + c;

+  {

+    if (a + b <= b + c && a + b <= a + c) {

+      this.num := a + b;

+      // repr stuff

+      this.Repr := {this};

+    } else {

+      if (a + c <= a + b && a + c <= b + c) {

+        this.num := a + c;

+        // repr stuff

+        this.Repr := {this};

+      } else {

+        this.num := b + c;

+        // repr stuff

+        this.Repr := {this};

+      }

+    }

+  }

+

+

+  method Min32(a: int, b: int, c: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures num in {a, b, c};

+    ensures (forall x :: x in {a, b, c} ==> num <= x);

+  {

+    if (a <= b && a <= c) {

+      this.num := a;

+      // repr stuff

+      this.Repr := {this};

+    } else {

+      if (c <= a && c <= b) {

+        this.num := c;

+        // repr stuff

+        this.Repr := {this};

+      } else {

+        this.num := b;

+        // repr stuff

+        this.Repr := {this};

+      }

+    }

+  }

+

+

+  method Min3(a: int, b: int, c: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures num in {a, b, c};

+    ensures num <= a;

+    ensures num <= b;

+    ensures num <= c;

+  {

+    if (a <= b && a <= c) {

+      this.num := a;

+      // repr stuff

+      this.Repr := {this};

+    } else {

+      if (c <= a && c <= b) {

+        this.num := c;

+        // repr stuff

+        this.Repr := {this};

+      } else {

+        this.num := b;

+        // repr stuff

+        this.Repr := {this};

+      }

+    }

+  }

+

+

+  method Min22(a: int, b: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures num in {a, b};

+    ensures num <= a;

+    ensures num <= b;

+  {

+    if (a <= b) {

+      this.num := a;

+      // repr stuff

+      this.Repr := {this};

+    } else {

+      this.num := b;

+      // repr stuff

+      this.Repr := {this};

+    }

+  }

+

+

+  method Min2(a: int, b: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures a < b ==> num == a;

+    ensures a >= b ==> num == b;

+  {

+    if (a >= b ==> a == b) {

+      this.num := a;

+      // repr stuff

+      this.Repr := {this};

+    } else {

+      this.num := b;

+      // repr stuff

+      this.Repr := {this};

+    }

+  }

+

+}

+

+

diff --git a/Source/Jennisys/examples/mod/jennisys-synth_Set.dfy b/Source/Jennisys/examples/mod/jennisys-synth_Set.dfy
new file mode 100644
index 00000000..40404bfb
--- /dev/null
+++ b/Source/Jennisys/examples/mod/jennisys-synth_Set.dfy
@@ -0,0 +1,388 @@
+class Set {

+  ghost var Repr: set<object>;

+  ghost var elems: set<int>;

+

+  var root: SetNode;

+

+  function Valid_repr(): bool

+    reads *;

+  {

+    this in Repr &&

+    null !in Repr &&

+    (root != null ==> root in Repr && root.Repr <= Repr && this !in root.Repr)

+  }

+

+  function Valid_self(): bool

+    reads *;

+  {

+    Valid_repr() &&

+    (root == null ==> elems == {}) &&

+    (root != null ==> elems == root.elems)

+  }

+

+  function Valid(): bool

+    reads *;

+  {

+    this.Valid_self() &&

+    (root != null ==> root.Valid())

+  }

+

+

+  method Double(p: int, q: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures elems == {p, q};

+  {

+    var gensym67 := new SetNode;

+    gensym67._synth_Set_Double_gensym67(p, q);

+    this.elems := {p, q};

+    this.root := gensym67;

+    // repr stuff

+    this.Repr := {this} + this.root.Repr;

+  }

+

+

+  method Empty()

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures elems == {};

+  {

+    this.elems := {};

+    this.root := null;

+    // repr stuff

+    this.Repr := {this};

+  }

+

+

+  method Singleton(t: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures elems == {t};

+  {

+    var gensym67 := new SetNode;

+    gensym67._synth_Set_Singleton_gensym67(t);

+    this.elems := {t};

+    this.root := gensym67;

+    // repr stuff

+    this.Repr := {this} + this.root.Repr;

+  }

+

+

+  method Sum(p: int, q: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures elems == {p + q};

+  {

+    var gensym69 := new SetNode;

+    gensym69._synth_Set_Sum_gensym69(p, q);

+    this.elems := {p + q};

+    this.root := gensym69;

+    // repr stuff

+    this.Repr := {this} + this.root.Repr;

+  }

+

+}

+

+class SetNode {

+  ghost var Repr: set<object>;

+  ghost var elems: set<int>;

+

+  var data: int;

+  var left: SetNode;

+  var right: SetNode;

+

+  function Valid_repr(): bool

+    reads *;

+  {

+    this in Repr &&

+    null !in Repr &&

+    (left != null ==> left in Repr && left.Repr <= Repr && this !in left.Repr) &&

+    (right != null ==> right in Repr && right.Repr <= Repr && this !in right.Repr)

+  }

+

+  function Valid_self(): bool

+    reads *;

+  {

+    Valid_repr() &&

+    (elems == ({data} + (if left != null then left.elems else {})) + (if right != null then right.elems else {})) &&

+    (left != null ==> (forall e :: e in left.elems ==> e < data)) &&

+    (right != null ==> (forall e :: e in right.elems ==> e > data))

+  }

+

+  function Valid(): bool

+    reads *;

+  {

+    this.Valid_self() &&

+    (left != null ==> left.Valid_self()) &&

+    (right != null ==> right.Valid_self()) &&

+    (left != null && left.left != null ==> left.left.Valid_self()) &&

+    (left != null && left.right != null ==> left.right.Valid_self()) &&

+    (right != null && right.left != null ==> right.left.Valid_self()) &&

+    (right != null && right.right != null ==> right.right.Valid_self())

+  }

+

+

+  method Double(p: int, q: int)

+    modifies this;

+    requires p != q;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures elems == {p, q};

+  {

+    if (q > p) {

+      var gensym77 := new SetNode;

+      gensym77._synth_SetNode_Double_gensym77(q);

+      this.data := p;

+      this.elems := {p, q};

+      this.left := null;

+      this.right := gensym77;

+      // repr stuff

+      this.Repr := {this} + this.right.Repr;

+    } else {

+      var gensym77 := new SetNode;

+      gensym77._synth_SetNode_Double_gensym77(p);

+      this.data := q;

+      this.elems := {p, q};

+      this.left := null;

+      this.right := gensym77;

+      // repr stuff

+      this.Repr := {this} + this.right.Repr;

+    }

+  }

+

+

+  method _synth_SetNode_Double_gensym77(q: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures elems == {q};

+  {

+    this.data := q;

+    this.elems := {q};

+    this.left := null;

+    this.right := null;

+    // repr stuff

+    this.Repr := {this};

+  }

+

+

+  method _synth_SetNode_Triple_gensym80(r: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures elems == {r};

+  {

+    this.data := r;

+    this.elems := {r};

+    this.left := null;

+    this.right := null;

+    // repr stuff

+    this.Repr := {this};

+  }

+

+

+  method Triple(p: int, q: int, r: int)

+    modifies this;

+    requires p != q;

+    requires q != r;

+    requires r != p;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures elems == {p, q, r};

+  {

+    if (p < q && r > q) {

+      var gensym80 := new SetNode;

+      var gensym81 := new SetNode;

+      gensym80._synth_SetNode_Triple_gensym80(r);

+      gensym81._synth_SetNode_Triple_gensym81(p);

+      this.data := q;

+      this.elems := {p, q, r};

+      this.left := gensym81;

+      this.right := gensym80;

+      // repr stuff

+      this.Repr := ({this} + this.left.Repr) + this.right.Repr;

+    } else {

+      if (r < p && q > p) {

+        var gensym80 := new SetNode;

+        var gensym81 := new SetNode;

+        gensym80._synth_SetNode_Triple_gensym80(q);

+        gensym81._synth_SetNode_Triple_gensym81(r);

+        this.data := p;

+        this.elems := {p, q, r};

+        this.left := gensym81;

+        this.right := gensym80;

+        // repr stuff

+        this.Repr := ({this} + this.left.Repr) + this.right.Repr;

+      } else {

+        if (p < r && q > r) {

+          var gensym80 := new SetNode;

+          var gensym81 := new SetNode;

+          gensym80._synth_SetNode_Triple_gensym80(q);

+          gensym81._synth_SetNode_Triple_gensym81(p);

+          this.data := r;

+          this.elems := {p, q, r};

+          this.left := gensym81;

+          this.right := gensym80;

+          // repr stuff

+          this.Repr := ({this} + this.left.Repr) + this.right.Repr;

+        } else {

+          if (r < q && p > q) {

+            var gensym80 := new SetNode;

+            var gensym81 := new SetNode;

+            gensym80._synth_SetNode_Triple_gensym80(p);

+            gensym81._synth_SetNode_Triple_gensym81(r);

+            this.data := q;

+            this.elems := {p, q, r};

+            this.left := gensym81;

+            this.right := gensym80;

+            // repr stuff

+            this.Repr := ({this} + this.left.Repr) + this.right.Repr;

+          } else {

+            if (q < r && p > r) {

+              var gensym80 := new SetNode;

+              var gensym81 := new SetNode;

+              gensym80._synth_SetNode_Triple_gensym80(p);

+              gensym81._synth_SetNode_Triple_gensym81(q);

+              this.data := r;

+              this.elems := {p, q, r};

+              this.left := gensym81;

+              this.right := gensym80;

+              // repr stuff

+              this.Repr := ({this} + this.left.Repr) + this.right.Repr;

+            } else {

+              var gensym80 := new SetNode;

+              var gensym81 := new SetNode;

+              gensym80._synth_SetNode_Triple_gensym80(r);

+              gensym81._synth_SetNode_Triple_gensym81(q);

+              this.data := p;

+              this.elems := {p, q, r};

+              this.left := gensym81;

+              this.right := gensym80;

+              // repr stuff

+              this.Repr := ({this} + this.left.Repr) + this.right.Repr;

+            }

+          }

+        }

+      }

+    }

+  }

+

+

+  method _synth_SetNode_Triple_gensym81(p: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures elems == {p};

+  {

+    this.data := p;

+    this.elems := {p};

+    this.left := null;

+    this.right := null;

+    // repr stuff

+    this.Repr := {this};

+  }

+

+

+  method Init(t: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures elems == {t};

+  {

+    this.data := t;

+    this.elems := {t};

+    this.left := null;

+    this.right := null;

+    // repr stuff

+    this.Repr := {this};

+  }

+

+

+  method _synth_SetNode__synth_Set_Double_gensym67_gensym77(q: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures elems == {q};

+  {

+    this.data := q;

+    this.elems := {q};

+    this.left := null;

+    this.right := null;

+    // repr stuff

+    this.Repr := {this};

+  }

+

+

+  method _synth_Set_Double_gensym67(p: int, q: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures elems == {p, q};

+  {

+    if (q > p) {

+      var gensym77 := new SetNode;

+      gensym77._synth_SetNode__synth_Set_Double_gensym67_gensym77(q);

+      this.data := p;

+      this.elems := {p, q};

+      this.left := null;

+      this.right := gensym77;

+      // repr stuff

+      this.Repr := {this} + this.right.Repr;

+    } else {

+      if (p > q) {

+        var gensym77 := new SetNode;

+        gensym77._synth_SetNode__synth_Set_Double_gensym67_gensym77(p);

+        this.data := q;

+        this.elems := {p, q};

+        this.left := null;

+        this.right := gensym77;

+        // repr stuff

+        this.Repr := {this} + this.right.Repr;

+      } else {

+        this.data := q;

+        this.elems := {p, q};

+        this.left := null;

+        this.right := null;

+        // repr stuff

+        this.Repr := {this};

+      }

+    }

+  }

+

+

+  method _synth_Set_Singleton_gensym67(t: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures elems == {t};

+  {

+    this.data := t;

+    this.elems := {t};

+    this.left := null;

+    this.right := null;

+    // repr stuff

+    this.Repr := {this};

+  }

+

+

+  method _synth_Set_Sum_gensym69(p: int, q: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures elems == {p + q};

+  {

+    this.data := p + q;

+    this.elems := {p + q};

+    this.left := null;

+    this.right := null;

+    // repr stuff

+    this.Repr := {this};

+  }

+

+}

+

+

diff --git a/Source/Jennisys/examples/mod2/jennisys-synth_DList.dfy b/Source/Jennisys/examples/mod2/jennisys-synth_DList.dfy
new file mode 100644
index 00000000..3e1aa99f
--- /dev/null
+++ b/Source/Jennisys/examples/mod2/jennisys-synth_DList.dfy
@@ -0,0 +1,255 @@
+class DList<T> {

+  ghost var Repr: set<object>;

+  ghost var list: seq<T>;

+

+  var root: DNode<T>;

+

+  function Valid_repr(): bool

+    reads *;

+  {

+    this in Repr &&

+    null !in Repr &&

+    (root != null ==> root in Repr && root.Repr <= Repr && this !in root.Repr)

+  }

+

+  function Valid_self(): bool

+    reads *;

+  {

+    Valid_repr() &&

+    (root == null ==> |list| == 0) &&

+    (root != null ==> list == root.list)

+  }

+

+  function Valid(): bool

+    reads *;

+  {

+    this.Valid_self() &&

+    (root != null ==> root.Valid())

+  }

+

+

+  method Double(p: T, q: T)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures list == [p, q];

+    ensures list[0] == p;

+    ensures list[1] == q;

+    ensures |list| == 2;

+  {

+    var gensym79 := new DNode<T>;

+    var gensym85 := new DNode<T>;

+    this.list := [p, q];

+    this.root := gensym79;

+    gensym79.data := p;

+    gensym79.list := [p, q];

+    gensym79.next := gensym85;

+    gensym79.prev := null;

+    gensym85.data := q;

+    gensym85.list := [q];

+    gensym85.next := null;

+    gensym85.prev := gensym79;

+

+    // repr stuff

+    gensym85.Repr := {gensym85};

+    gensym79.Repr := {gensym79} + {gensym85};

+    this.Repr := {this} + ({gensym79} + {gensym85});

+    // assert repr objects are valid (helps verification)

+    assert gensym79.Valid() && gensym85.Valid();

+  }

+

+

+  method Empty()

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures list == [];

+    ensures |list| == 0;

+  {

+    this.list := [];

+    this.root := null;

+

+    // repr stuff

+    this.Repr := {this};

+  }

+

+

+  method Singleton(t: T)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures list == [t];

+    ensures list[0] == t;

+    ensures |list| == 1;

+  {

+    var gensym78 := new DNode<T>;

+    this.list := [t];

+    this.root := gensym78;

+    gensym78.data := t;

+    gensym78.list := [t];

+    gensym78.next := null;

+    gensym78.prev := null;

+

+    // repr stuff

+    gensym78.Repr := {gensym78};

+    this.Repr := {this} + {gensym78};

+    // assert repr objects are valid (helps verification)

+    assert gensym78.Valid();

+  }

+

+}

+

+class DNode<T> {

+  ghost var Repr: set<object>;

+  ghost var list: seq<T>;

+

+  var data: T;

+  var next: DNode<T>;

+  var prev: DNode<T>;

+

+  function Valid_repr(): bool

+    reads *;

+  {

+    this in Repr &&

+    null !in Repr &&

+    (next != null ==> next in Repr && next.Repr <= Repr && this !in next.Repr)

+  }

+

+  function Valid_self(): bool

+    reads *;

+  {

+    Valid_repr() &&

+    (next == null ==> (list == [data] && list[0] == data) && |list| == 1) &&

+    (next != null ==> list == [data] + next.list && next.prev == this) &&

+    (prev != null ==> prev.next == this) &&

+    (|list| > 0)

+  }

+

+  function Valid(): bool

+    reads *;

+    decreases Repr;

+  {

+    this.Valid_self() &&

+    (next != null ==> next.Valid()) &&

+    (next != null ==> next.Valid_self()) &&

+    (next != null && next.next != null ==> next.next.Valid_self())

+  }

+

+

+  method Double(p: T, q: T)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures list == [p, q];

+    ensures list[0] == p;

+    ensures list[1] == q;

+    ensures |list| == 2;

+  {

+    var gensym95 := new DNode<T>;

+    this.data := p;

+    this.list := [p, q];

+    this.next := gensym95;

+    this.prev := null;

+    gensym95.data := q;

+    gensym95.list := [q];

+    gensym95.next := null;

+    gensym95.prev := this;

+

+    // repr stuff

+    this.Repr := {this} + {gensym95};

+    gensym95.Repr := {gensym95};

+    // assert repr objects are valid (helps verification)

+    assert gensym95.Valid();

+  }

+

+

+  method Find(n: T) returns (ret: bool)

+    requires Valid();

+    ensures fresh(Repr - old(Repr));

+    ensures Valid();

+    ensures ret == (n in list);

+    decreases Repr;

+  {

+    if (this.next == null) {

+      ret := n == this.data;

+    } else {

+      var x_5 := this.next.Find(n);

+      ret := n == this.data || x_5;

+    }

+  }

+

+

+  method Get(idx: int) returns (ret: T)

+    requires Valid();

+    requires idx >= 0;

+    requires idx < |list|;

+    ensures fresh(Repr - old(Repr));

+    ensures Valid();

+    ensures ret == list[idx];

+    decreases Repr;

+  {

+    if (this.next == null) {

+      ret := this.data;

+    } else {

+      if (idx == 0) {

+        ret := this.data;

+      } else {

+        var x_6 := this.next.Get(idx - 1);

+        ret := x_6;

+      }

+    }

+  }

+

+

+  method Init(t: T)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures list == [t];

+    ensures list[0] == t;

+    ensures |list| == 1;

+  {

+    this.data := t;

+    this.list := [t];

+    this.next := null;

+    this.prev := null;

+

+    // repr stuff

+    this.Repr := {this};

+  }

+

+

+  method List() returns (ret: seq<T>)

+    requires Valid();

+    ensures fresh(Repr - old(Repr));

+    ensures Valid();

+    ensures ret == list;

+    decreases Repr;

+  {

+    if (this.next == null) {

+      ret := [this.data];

+    } else {

+      var x_7 := this.next.List();

+      ret := [this.data] + x_7;

+    }

+  }

+

+

+  method Size() returns (ret: int)

+    requires Valid();

+    ensures fresh(Repr - old(Repr));

+    ensures Valid();

+    ensures ret == |list|;

+    decreases Repr;

+  {

+    if (this.next == null) {

+      ret := 1;

+    } else {

+      var x_8 := this.next.Size();

+      ret := 1 + x_8;

+    }

+  }

+

+}

+

+

diff --git a/Source/Jennisys/examples/mod2/jennisys-synth_List.dfy b/Source/Jennisys/examples/mod2/jennisys-synth_List.dfy
new file mode 100644
index 00000000..9939dcc2
--- /dev/null
+++ b/Source/Jennisys/examples/mod2/jennisys-synth_List.dfy
@@ -0,0 +1,249 @@
+class List<T> {

+  ghost var Repr: set<object>;

+  ghost var list: seq<T>;

+

+  var root: Node<T>;

+

+  function Valid_repr(): bool

+    reads *;

+  {

+    this in Repr &&

+    null !in Repr &&

+    (root != null ==> root in Repr && root.Repr <= Repr && this !in root.Repr)

+  }

+

+  function Valid_self(): bool

+    reads *;

+  {

+    Valid_repr() &&

+    (root == null ==> |list| == 0) &&

+    (root != null ==> list == root.list)

+  }

+

+  function Valid(): bool

+    reads *;

+  {

+    this.Valid_self() &&

+    (root != null ==> root.Valid())

+  }

+

+

+  method Double(p: T, q: T)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures list == [p, q];

+    ensures list[0] == p;

+    ensures list[1] == q;

+    ensures |list| == 2;

+  {

+    var gensym78 := new Node<T>;

+    gensym78.Double(p, q);

+    this.list := [p, q];

+    this.root := gensym78;

+

+    // repr stuff

+    this.Repr := {this} + this.root.Repr;

+    // assert repr objects are valid (helps verification)

+    assert gensym78.Valid();

+  }

+

+

+  method Empty()

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures list == [];

+    ensures |list| == 0;

+  {

+    this.list := [];

+    this.root := null;

+

+    // repr stuff

+    this.Repr := {this};

+  }

+

+

+  method Singleton(t: T)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures list == [t];

+    ensures list[0] == t;

+    ensures |list| == 1;

+  {

+    var gensym77 := new Node<T>;

+    gensym77.Init(t);

+    this.list := [t];

+    this.root := gensym77;

+

+    // repr stuff

+    this.Repr := {this} + this.root.Repr;

+    // assert repr objects are valid (helps verification)

+    assert gensym77.Valid();

+  }

+

+}

+

+class Node<T> {

+  ghost var Repr: set<object>;

+  ghost var list: seq<T>;

+

+  var data: T;

+  var next: Node<T>;

+

+  function Valid_repr(): bool

+    reads *;

+  {

+    this in Repr &&

+    null !in Repr &&

+    (next != null ==> next in Repr && next.Repr <= Repr && this !in next.Repr)

+  }

+

+  function Valid_self(): bool

+    reads *;

+  {

+    Valid_repr() &&

+    (next == null ==> (list == [data] && list[0] == data) && |list| == 1) &&

+    (next != null ==> list == [data] + next.list) &&

+    (|list| > 0)

+  }

+

+  function Valid(): bool

+    reads *;

+    decreases Repr;

+  {

+    this.Valid_self() &&

+    (next != null ==> next.Valid()) &&

+    (next != null ==> next.Valid_self()) &&

+    (next != null && next.next != null ==> next.next.Valid_self())

+  }

+

+

+  method Double(p: T, q: T)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures list == [p, q];

+    ensures list[0] == p;

+    ensures list[1] == q;

+    ensures |list| == 2;

+  {

+    var gensym87 := new Node<T>;

+    gensym87.Init(q);

+    this.data := p;

+    this.list := [p, q];

+    this.next := gensym87;

+

+    // repr stuff

+    this.Repr := {this} + this.next.Repr;

+    // assert repr objects are valid (helps verification)

+    assert gensym87.Valid();

+  }

+

+

+  method Find(n: T) returns (ret: bool)

+    requires Valid();

+    ensures fresh(Repr - old(Repr));

+    ensures Valid();

+    ensures ret == (n in list);

+    decreases Repr;

+  {

+    if (n != this.data && this.next == null) {

+      ret := n == this.data;

+    } else {

+      if (this.next != null) {

+        var x_6 := this.next.Find(n);

+        ret := n == this.data || x_6;

+      } else {

+        ret := true;

+      }

+    }

+  }

+

+

+  method Get(idx: int) returns (ret: T)

+    requires Valid();

+    requires idx >= 0;

+    requires idx < |list|;

+    ensures fresh(Repr - old(Repr));

+    ensures Valid();

+    ensures ret == list[idx];

+    decreases Repr;

+  {

+    if (this.next == null) {

+      ret := this.data;

+    } else {

+      if (idx == 0) {

+        ret := this.data;

+      } else {

+        var x_7 := this.next.Get(idx - 1);

+        ret := x_7;

+      }

+    }

+  }

+

+

+  method Init(t: T)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures list == [t];

+    ensures list[0] == t;

+    ensures |list| == 1;

+  {

+    this.data := t;

+    this.list := [t];

+    this.next := null;

+

+    // repr stuff

+    this.Repr := {this};

+  }

+

+

+  method List() returns (ret: seq<T>)

+    requires Valid();

+    ensures fresh(Repr - old(Repr));

+    ensures Valid();

+    ensures ret == list;

+    decreases Repr;

+  {

+    if (this.next == null) {

+      ret := [this.data];

+    } else {

+      var x_8 := this.next.List();

+      ret := [this.data] + x_8;

+    }

+  }

+

+

+  method Size() returns (ret: int)

+    requires Valid();

+    ensures fresh(Repr - old(Repr));

+    ensures Valid();

+    ensures ret == |list|;

+    decreases Repr;

+  {

+    if (this.next == null) {

+      ret := 1;

+    } else {

+      var x_9 := this.next.Size();

+      ret := 1 + x_9;

+    }

+  }

+

+

+  method Tail() returns (tail: Node<T>)

+    requires Valid();

+    ensures fresh(Repr - old(Repr));

+    ensures Valid();

+    ensures |list| == 1 ==> tail == null;

+    ensures |list| > 1 ==> tail != null && tail.list == list[1..];

+    ensures tail != null ==> tail.Valid();

+  {

+    tail := this.next;

+  }

+

+}

+

+

diff --git a/Source/Jennisys/examples/mod2/jennisys-synth_List2.dfy b/Source/Jennisys/examples/mod2/jennisys-synth_List2.dfy
new file mode 100644
index 00000000..f994186b
--- /dev/null
+++ b/Source/Jennisys/examples/mod2/jennisys-synth_List2.dfy
@@ -0,0 +1,225 @@
+class IntList {

+  ghost var Repr: set<object>;

+  ghost var list: seq<int>;

+

+  var root: IntNode;

+

+  function Valid_repr(): bool

+    reads *;

+  {

+    this in Repr &&

+    null !in Repr &&

+    (root != null ==> root in Repr && root.Repr <= Repr && this !in root.Repr)

+  }

+

+  function Valid_self(): bool

+    reads *;

+  {

+    Valid_repr() &&

+    (root == null <==> |list| == 0) &&

+    (root != null ==> list == root.list)

+  }

+

+  function Valid(): bool

+    reads *;

+  {

+    this.Valid_self() &&

+    (root != null ==> root.Valid())

+  }

+

+

+  method Double(p: int, q: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures list == [p] + [q];

+    ensures list[0] == p;

+    ensures list[1] == q;

+    ensures |list| == 2;

+  {

+    var gensym74 := new IntNode;

+    gensym74.Double(p, q);

+    this.list := [p] + [q];

+    this.root := gensym74;

+

+    // repr stuff

+    this.Repr := {this} + this.root.Repr;

+    // assert repr objects are valid (helps verification)

+    assert gensym74.Valid();

+  }

+

+

+  method Empty()

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures list == [];

+    ensures |list| == 0;

+  {

+    this.list := [];

+    this.root := null;

+

+    // repr stuff

+    this.Repr := {this};

+  }

+

+

+  method OneTwo()

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures list == [1, 2];

+    ensures list[0] == 1;

+    ensures list[1] == 2;

+    ensures |list| == 2;

+  {

+    this.Double(1, 2);

+  }

+

+

+  method Singleton(p: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures list == [p];

+    ensures list[0] == p;

+    ensures |list| == 1;

+  {

+    var gensym73 := new IntNode;

+    gensym73.Init(p);

+    this.list := [p];

+    this.root := gensym73;

+

+    // repr stuff

+    this.Repr := {this} + this.root.Repr;

+    // assert repr objects are valid (helps verification)

+    assert gensym73.Valid();

+  }

+

+

+  method SingletonTwo()

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures list == [2];

+    ensures list[0] == 2;

+    ensures |list| == 1;

+  {

+    this.Singleton(2);

+  }

+

+

+  method Sum(p: int, q: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures list == [p + q];

+    ensures list[0] == p + q;

+    ensures |list| == 1;

+  {

+    this.Singleton(p + q);

+  }

+

+

+  method TwoConsecutive(p: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures list == [p] + [p + 1];

+    ensures list[0] == p;

+    ensures list[1] == p + 1;

+    ensures |list| == 2;

+  {

+    this.Double(p, p + 1);

+  }

+

+}

+

+class IntNode {

+  ghost var Repr: set<object>;

+  ghost var list: seq<int>;

+

+  var data: int;

+  var next: IntNode;

+

+  function Valid_repr(): bool

+    reads *;

+  {

+    this in Repr &&

+    null !in Repr &&

+    (next != null ==> next in Repr && next.Repr <= Repr && this !in next.Repr)

+  }

+

+  function Valid_self(): bool

+    reads *;

+  {

+    Valid_repr() &&

+    (next == null ==> (list == [data] && list[0] == data) && |list| == 1) &&

+    (next != null ==> list == [data] + next.list) &&

+    (|list| > 0)

+  }

+

+  function Valid(): bool

+    reads *;

+    decreases Repr;

+  {

+    this.Valid_self() &&

+    (next != null ==> next.Valid()) &&

+    (next != null ==> next.Valid_self()) &&

+    (next != null && next.next != null ==> next.next.Valid_self())

+  }

+

+

+  method Double(x: int, y: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures list == [x, y];

+    ensures list[0] == x;

+    ensures list[1] == y;

+    ensures |list| == 2;

+  {

+    var gensym87 := new IntNode;

+    gensym87.Init(y);

+    this.data := x;

+    this.list := [x, y];

+    this.next := gensym87;

+

+    // repr stuff

+    this.Repr := {this} + this.next.Repr;

+    // assert repr objects are valid (helps verification)

+    assert gensym87.Valid();

+  }

+

+

+  method Init(x: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures list == [x];

+    ensures list[0] == x;

+    ensures |list| == 1;

+  {

+    this.data := x;

+    this.list := [x];

+    this.next := null;

+

+    // repr stuff

+    this.Repr := {this};

+  }

+

+

+  method SingletonZero()

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures list == [0];

+    ensures list[0] == 0;

+    ensures |list| == 1;

+  {

+    this.Init(0);

+  }

+

+}

+

+

diff --git a/Source/Jennisys/examples/mod2/jennisys-synth_List3.dfy b/Source/Jennisys/examples/mod2/jennisys-synth_List3.dfy
new file mode 100644
index 00000000..65e308bd
--- /dev/null
+++ b/Source/Jennisys/examples/mod2/jennisys-synth_List3.dfy
@@ -0,0 +1,309 @@
+class IntList {

+  ghost var Repr: set<object>;

+  ghost var list: seq<int>;

+

+  var root: IntNode;

+

+  function Valid_repr(): bool

+    reads *;

+  {

+    this in Repr &&

+    null !in Repr &&

+    (root != null ==> root in Repr && root.Repr <= Repr && this !in root.Repr)

+  }

+

+  function Valid_self(): bool

+    reads *;

+  {

+    Valid_repr() &&

+    (root == null ==> |list| == 0) &&

+    (root != null ==> |list| == |root.succ| + 1 && (list[0] == root.data && (forall i :: 1 <= i && i <= |root.succ| ==> root.succ[i - 1] != null && list[i] == root.succ[i - 1].data)))

+  }

+

+  function Valid(): bool

+    reads *;

+  {

+    this.Valid_self() &&

+    (root != null ==> root.Valid())

+  }

+

+

+  method Double(p: int, q: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures list == [p] + [q];

+    ensures list[0] == p;

+    ensures list[1] == q;

+    ensures |list| == 2;

+  {

+    var gensym79 := new IntNode;

+    gensym79._synth_IntList_Double_gensym79(p, q);

+    this.list := [p] + [q];

+    this.root := gensym79;

+

+    // repr stuff

+    this.Repr := {this} + this.root.Repr;

+    // assert repr objects are valid (helps verification)

+    assert gensym79.Valid();

+  }

+

+

+  method Empty()

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures list == [];

+    ensures |list| == 0;

+  {

+    this.list := [];

+    this.root := null;

+

+    // repr stuff

+    this.Repr := {this};

+  }

+

+

+  method OneTwo()

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures list == [1, 2];

+    ensures list[0] == 1;

+    ensures list[1] == 2;

+    ensures |list| == 2;

+  {

+    this.Double(1, 2);

+  }

+

+

+  method Singleton(p: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures list == [p];

+    ensures list[0] == p;

+    ensures |list| == 1;

+  {

+    var gensym77 := new IntNode;

+    gensym77._synth_IntList_Singleton_gensym77(p);

+    this.list := [p];

+    this.root := gensym77;

+

+    // repr stuff

+    this.Repr := {this} + this.root.Repr;

+    // assert repr objects are valid (helps verification)

+    assert gensym77.Valid();

+  }

+

+

+  method SingletonTwo()

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures list == [2];

+    ensures list[0] == 2;

+    ensures |list| == 1;

+  {

+    this.Singleton(2);

+  }

+

+

+  method Sum(p: int, q: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures list == [p + q];

+    ensures list[0] == p + q;

+    ensures |list| == 1;

+  {

+    this.Singleton(p + q);

+  }

+

+

+  method TwoConsecutive(p: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures list == [p] + [p + 1];

+    ensures list[0] == p;

+    ensures list[1] == p + 1;

+    ensures |list| == 2;

+  {

+    this.Double(p, p + 1);

+  }

+

+}

+

+class IntNode {

+  ghost var Repr: set<object>;

+  ghost var succ: seq<IntNode>;

+  ghost var data: int;

+

+  var next: IntNode;

+

+  function Valid_repr(): bool

+    reads *;

+  {

+    this in Repr &&

+    null !in Repr &&

+    (next != null ==> next in Repr && next.Repr <= Repr && this !in next.Repr)

+  }

+

+  function Valid_self(): bool

+    reads *;

+  {

+    Valid_repr() &&

+    (next == null ==> |succ| == 0) &&

+    (next != null ==> succ == [next] + next.succ) &&

+    (!(null in succ))

+  }

+

+  function Valid(): bool

+    reads *;

+    decreases Repr;

+  {

+    this.Valid_self() &&

+    (next != null ==> next.Valid()) &&

+    (next != null ==> next.Valid_self()) &&

+    (next != null && next.next != null ==> next.next.Valid_self())

+  }

+

+

+  method Init(p: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures data == p;

+  {

+    this.data := p;

+    this.next := null;

+    this.succ := [];

+

+    // repr stuff

+    this.Repr := {this};

+  }

+

+

+  method InitInc(p: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures data == p + 1;

+  {

+    this.Init(p + 1);

+  }

+

+

+  method OneTwo()

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures data == 1;

+    ensures |succ| == 1;

+    ensures succ[0] != null;

+    ensures succ[0].data == 2;

+  {

+    var gensym83 := new IntNode;

+    gensym83._synth_IntNode_OneTwo_gensym83();

+    this.data := 1;

+    this.next := gensym83;

+    this.succ := [gensym83];

+

+    // repr stuff

+    this.Repr := {this} + this.next.Repr;

+    // assert repr objects are valid (helps verification)

+    assert gensym83.Valid();

+  }

+

+

+  method Zero()

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures data == 0;

+    ensures succ == [];

+    ensures |succ| == 0;

+  {

+    this.data := 0;

+    this.next := null;

+    this.succ := [];

+

+    // repr stuff

+    this.Repr := {this};

+  }

+

+

+  method _synth_IntList_Double_gensym79(p: int, q: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures data == p;

+    ensures |succ| == 1;

+    ensures succ[0].data == q;

+    ensures succ[0].succ == [];

+    ensures |succ[0].succ| == 0;

+  {

+    var gensym93 := new IntNode;

+    gensym93._synth_IntNode__synth_IntList_Double_gensym79_gensym93(q);

+    this.data := p;

+    this.next := gensym93;

+    this.succ := [gensym93];

+

+    // repr stuff

+    this.Repr := {this} + this.next.Repr;

+    // assert repr objects are valid (helps verification)

+    assert gensym93.Valid();

+  }

+

+

+  method _synth_IntList_Singleton_gensym77(p: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures data == p;

+    ensures |succ| == 0;

+  {

+    this.data := p;

+    this.next := null;

+    this.succ := [];

+

+    // repr stuff

+    this.Repr := {this};

+  }

+

+

+  method _synth_IntNode_OneTwo_gensym83()

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures data == 2;

+    ensures |succ| == 0;

+  {

+    this.data := 2;

+    this.next := null;

+    this.succ := [];

+

+    // repr stuff

+    this.Repr := {this};

+  }

+

+

+  method _synth_IntNode__synth_IntList_Double_gensym79_gensym93(q: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures data == q;

+    ensures |succ| == 0;

+  {

+    this.data := q;

+    this.next := null;

+    this.succ := [];

+

+    // repr stuff

+    this.Repr := {this};

+  }

+

+}

+

+

diff --git a/Source/Jennisys/examples/mod2/jennisys-synth_Number.dfy b/Source/Jennisys/examples/mod2/jennisys-synth_Number.dfy
new file mode 100644
index 00000000..9bb3c398
--- /dev/null
+++ b/Source/Jennisys/examples/mod2/jennisys-synth_Number.dfy
@@ -0,0 +1,181 @@
+class Number {

+  ghost var Repr: set<object>;

+  ghost var num: int;

+

+

+  function Valid_repr(): bool

+    reads *;

+  {

+    this in Repr &&

+    null !in Repr

+  }

+

+  function Valid_self(): bool

+    reads *;

+  {

+    Valid_repr() &&

+    true

+  }

+

+  function Valid(): bool

+    reads *;

+  {

+    this.Valid_self() &&

+    true

+  }

+

+

+  method Abs(a: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures num in {a, -a};

+    ensures num >= 0;

+  {

+    if (a >= 0) {

+      this.Init(a);

+    } else {

+      this.Init(-a);

+    }

+  }

+

+

+  method Double(p: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures num == 2 * p;

+  {

+    this.Init(2 * p);

+  }

+

+

+  method Init(p: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures num == p;

+  {

+    this.num := p;

+

+    // repr stuff

+    this.Repr := {this};

+  }

+

+

+  method Min2(a: int, b: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures a < b ==> num == a;

+    ensures a >= b ==> num == b;

+  {

+    if (a < b) {

+      this.Init(a);

+    } else {

+      this.Init(b);

+    }

+  }

+

+

+  method Min22(a: int, b: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures num in {a, b};

+    ensures num <= a;

+    ensures num <= b;

+  {

+    if (a <= b) {

+      this.Init(a);

+    } else {

+      this.Init(b);

+    }

+  }

+

+

+  method Min3(a: int, b: int, c: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures num in {a, b, c};

+    ensures num <= a;

+    ensures num <= b;

+    ensures num <= c;

+  {

+    this.Min32(a, b, c);

+  }

+

+

+  method Min32(a: int, b: int, c: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures num in {a, b, c};

+    ensures num <= a;

+    ensures num <= b;

+    ensures num <= c;

+  {

+    if (a <= b && a <= c) {

+      this.Init(a);

+    } else {

+      if (c <= a && c <= b) {

+        this.Init(c);

+      } else {

+        this.Init(b);

+      }

+    }

+  }

+

+

+  method Min4(a: int, b: int, c: int, d: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures num in {a, b, c, d};

+    ensures num <= a;

+    ensures num <= b;

+    ensures num <= c;

+    ensures num <= d;

+  {

+    if ((a <= b && a <= c) && a <= d) {

+      this.Init(a);

+    } else {

+      if ((d <= a && d <= b) && d <= c) {

+        this.Init(d);

+      } else {

+        if ((c <= a && c <= b) && c <= d) {

+          this.Init(c);

+        } else {

+          this.Init(b);

+        }

+      }

+    }

+  }

+

+

+  method MinSum(a: int, b: int, c: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures num in {a + b, a + c, b + c};

+    ensures num <= a + b;

+    ensures num <= b + c;

+    ensures num <= a + c;

+  {

+    this.Min3(a + b, b + c, a + c);

+  }

+

+

+  method Sum(a: int, b: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures num == a + b;

+  {

+    this.Init(a + b);

+  }

+

+}

+

+

diff --git a/Source/Jennisys/examples/mod2/jennisys-synth_NumberMethods.dfy b/Source/Jennisys/examples/mod2/jennisys-synth_NumberMethods.dfy
new file mode 100644
index 00000000..b20e2741
--- /dev/null
+++ b/Source/Jennisys/examples/mod2/jennisys-synth_NumberMethods.dfy
@@ -0,0 +1,167 @@
+class NumberMethods {

+  ghost var Repr: set<object>;

+

+

+  function Valid_repr(): bool

+    reads *;

+  {

+    this in Repr &&

+    null !in Repr

+  }

+

+  function Valid_self(): bool

+    reads *;

+  {

+    Valid_repr() &&

+    true

+  }

+

+  function Valid(): bool

+    reads *;

+  {

+    this.Valid_self() &&

+    true

+  }

+

+

+  method Abs(a: int) returns (ret: int)

+    requires Valid();

+    ensures fresh(Repr - old(Repr));

+    ensures Valid();

+    ensures ret in {a, -a};

+    ensures ret >= 0;

+  {

+    if (-a >= 0) {

+      ret := -a;

+    } else {

+      ret := a;

+    }

+  }

+

+

+  method Double(p: int) returns (ret: int)

+    requires Valid();

+    ensures fresh(Repr - old(Repr));

+    ensures Valid();

+    ensures ret == 2 * p;

+  {

+    ret := 2 * p;

+  }

+

+

+  method Min2(a: int, b: int) returns (ret: int)

+    requires Valid();

+    ensures fresh(Repr - old(Repr));

+    ensures Valid();

+    ensures a < b ==> ret == a;

+    ensures a >= b ==> ret == b;

+  {

+    if (a < b) {

+      ret := a;

+    } else {

+      ret := b;

+    }

+  }

+

+

+  method Min22(a: int, b: int) returns (ret: int)

+    requires Valid();

+    ensures fresh(Repr - old(Repr));

+    ensures Valid();

+    ensures ret in {a, b};

+    ensures ret <= a;

+    ensures ret <= b;

+  {

+    if (a <= b) {

+      ret := a;

+    } else {

+      ret := b;

+    }

+  }

+

+

+  method Min3(a: int, b: int, c: int) returns (ret: int)

+    requires Valid();

+    ensures fresh(Repr - old(Repr));

+    ensures Valid();

+    ensures ret in {a, b, c};

+    ensures ret <= a;

+    ensures ret <= b;

+    ensures ret <= c;

+  {

+    ret := this.Min32(a, b, c);

+  }

+

+

+  method Min32(a: int, b: int, c: int) returns (ret: int)

+    requires Valid();

+    ensures fresh(Repr - old(Repr));

+    ensures Valid();

+    ensures ret in {a, b, c};

+    ensures ret <= a;

+    ensures ret <= b;

+    ensures ret <= c;

+  {

+    if (a <= b && a <= c) {

+      ret := a;

+    } else {

+      if (c <= a && c <= b) {

+        ret := c;

+      } else {

+        ret := b;

+      }

+    }

+  }

+

+

+  method Min4(a: int, b: int, c: int, d: int) returns (ret: int)

+    requires Valid();

+    ensures fresh(Repr - old(Repr));

+    ensures Valid();

+    ensures ret in {a, b, c, d};

+    ensures ret <= a;

+    ensures ret <= b;

+    ensures ret <= c;

+    ensures ret <= d;

+  {

+    if ((a <= b && a <= c) && a <= d) {

+      ret := a;

+    } else {

+      if ((d <= a && d <= b) && d <= c) {

+        ret := d;

+      } else {

+        if ((c <= a && c <= b) && c <= d) {

+          ret := c;

+        } else {

+          ret := b;

+        }

+      }

+    }

+  }

+

+

+  method MinSum(a: int, b: int, c: int) returns (ret: int)

+    requires Valid();

+    ensures fresh(Repr - old(Repr));

+    ensures Valid();

+    ensures ret in {a + b, a + c, b + c};

+    ensures ret <= a + b;

+    ensures ret <= b + c;

+    ensures ret <= a + c;

+  {

+    ret := this.Min3(a + b, b + c, a + c);

+  }

+

+

+  method Sum(a: int, b: int) returns (ret: int)

+    requires Valid();

+    ensures fresh(Repr - old(Repr));

+    ensures Valid();

+    ensures ret == a + b;

+  {

+    ret := a + b;

+  }

+

+}

+

+

diff --git a/Source/Jennisys/examples/mod2/jennisys-synth_Set.dfy b/Source/Jennisys/examples/mod2/jennisys-synth_Set.dfy
new file mode 100644
index 00000000..fea364d6
--- /dev/null
+++ b/Source/Jennisys/examples/mod2/jennisys-synth_Set.dfy
@@ -0,0 +1,304 @@
+class Set {

+  ghost var Repr: set<object>;

+  ghost var elems: set<int>;

+

+  var root: SetNode;

+

+  function Valid_repr(): bool

+    reads *;

+  {

+    this in Repr &&

+    null !in Repr &&

+    (root != null ==> root in Repr && root.Repr <= Repr && this !in root.Repr)

+  }

+

+  function Valid_self(): bool

+    reads *;

+  {

+    Valid_repr() &&

+    (root == null ==> elems == {}) &&

+    (root != null ==> elems == root.elems)

+  }

+

+  function Valid(): bool

+    reads *;

+  {

+    this.Valid_self() &&

+    (root != null ==> root.Valid())

+  }

+

+

+  method Double(p: int, q: int)

+    modifies this;

+    requires p != q;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures elems == {p, q};

+  {

+    var gensym80 := new SetNode;

+    gensym80.Double(p, q);

+    this.elems := {q, p};

+    this.root := gensym80;

+

+    // repr stuff

+    this.Repr := {this} + this.root.Repr;

+    // assert repr objects are valid (helps verification)

+    assert gensym80.Valid();

+  }

+

+

+  method Empty()

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures elems == {};

+  {

+    this.elems := {};

+    this.root := null;

+

+    // repr stuff

+    this.Repr := {this};

+  }

+

+

+  method Singleton(t: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures elems == {t};

+  {

+    var gensym75 := new SetNode;

+    gensym75.Init(t);

+    this.elems := {t};

+    this.root := gensym75;

+

+    // repr stuff

+    this.Repr := {this} + this.root.Repr;

+    // assert repr objects are valid (helps verification)

+    assert gensym75.Valid();

+  }

+

+

+  method SingletonZero()

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures elems == {0};

+  {

+    this.Singleton(0);

+  }

+

+

+  method Sum(p: int, q: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures elems == {p + q};

+  {

+    this.Singleton(p + q);

+  }

+

+}

+

+class SetNode {

+  ghost var Repr: set<object>;

+  ghost var elems: set<int>;

+

+  var data: int;

+  var left: SetNode;

+  var right: SetNode;

+

+  function Valid_repr(): bool

+    reads *;

+  {

+    this in Repr &&

+    null !in Repr &&

+    (left != null ==> left in Repr && left.Repr <= Repr && this !in left.Repr) &&

+    (right != null ==> right in Repr && right.Repr <= Repr && this !in right.Repr)

+  }

+

+  function Valid_self(): bool

+    reads *;

+  {

+    Valid_repr() &&

+    (elems == ({data} + (if left != null then left.elems else {})) + (if right != null then right.elems else {})) &&

+    (left != null ==> (forall e :: e in left.elems ==> e < data)) &&

+    (right != null ==> (forall e :: e in right.elems ==> e > data))

+  }

+

+  function Valid(): bool

+    reads *;

+    decreases Repr;

+  {

+    this.Valid_self() &&

+    (left != null ==> left.Valid()) &&

+    (right != null ==> right.Valid()) &&

+    (left != null ==> left.Valid_self()) &&

+    (right != null ==> right.Valid_self()) &&

+    (left != null && left.left != null ==> left.left.Valid_self()) &&

+    (left != null && left.right != null ==> left.right.Valid_self()) &&

+    (right != null && right.left != null ==> right.left.Valid_self()) &&

+    (right != null && right.right != null ==> right.right.Valid_self())

+  }

+

+

+  method Double(a: int, b: int)

+    modifies this;

+    requires a != b;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures elems == {a, b};

+  {

+    if (b > a) {

+      this.DoubleBase(b, a);

+    } else {

+      var gensym88 := new SetNode;

+      gensym88.Init(a);

+      this.data := b;

+      this.elems := {b, a};

+      this.left := null;

+      this.right := gensym88;

+

+      // repr stuff

+      this.Repr := {this} + this.right.Repr;

+      // assert repr objects are valid (helps verification)

+      assert gensym88.Valid();

+    }

+  }

+

+

+  method DoubleBase(x: int, y: int)

+    modifies this;

+    requires x > y;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures elems == {x, y};

+  {

+    var gensym88 := new SetNode;

+    gensym88.Init(x);

+    this.data := y;

+    this.elems := {y, x};

+    this.left := null;

+    this.right := gensym88;

+

+    // repr stuff

+    this.Repr := {this} + this.right.Repr;

+    // assert repr objects are valid (helps verification)

+    assert gensym88.Valid();

+  }

+

+

+  method Find(n: int) returns (ret: bool)

+    requires Valid();

+    ensures fresh(Repr - old(Repr));

+    ensures Valid();

+    ensures ret == (n in elems);

+    decreases Repr;

+  {

+    if (this.left != null && this.right != null) {

+      var x_9 := this.left.Find(n);

+      var x_10 := this.right.Find(n);

+      ret := (n == this.data || x_9) || x_10;

+    } else {

+      if (this.left != null && this.right == null) {

+        var x_11 := this.left.Find(n);

+        ret := n == this.data || x_11;

+      } else {

+        if (this.right != null && this.left == null) {

+          var x_12 := this.right.Find(n);

+          ret := n == this.data || x_12;

+        } else {

+          ret := n == this.data;

+        }

+      }

+    }

+  }

+

+

+  method Init(x: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures elems == {x};

+  {

+    this.data := x;

+    this.elems := {x};

+    this.left := null;

+    this.right := null;

+

+    // repr stuff

+    this.Repr := {this};

+  }

+

+

+  method Triple(x: int, y: int, z: int)

+    modifies this;

+    requires x != y;

+    requires y != z;

+    requires z != x;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures elems == {x, y, z};

+  {

+    if (z < x && y > x) {

+      this.TripleBase(z, x, y);

+    } else {

+      if (x < y && z > y) {

+        this.TripleBase(x, y, z);

+      } else {

+        if (x < z && y > z) {

+          this.TripleBase(x, z, y);

+        } else {

+          if (y < z && x > z) {

+            this.TripleBase(y, z, x);

+          } else {

+            if (z < y && x > y) {

+              this.TripleBase(z, y, x);

+            } else {

+              var gensym82 := new SetNode;

+              var gensym83 := new SetNode;

+              gensym82.Init(y);

+              gensym83.Init(z);

+              this.data := x;

+              this.elems := {y, x, z};

+              this.left := gensym82;

+              this.right := gensym83;

+

+              // repr stuff

+              this.Repr := ({this} + this.left.Repr) + this.right.Repr;

+              // assert repr objects are valid (helps verification)

+              assert gensym82.Valid() && gensym83.Valid();

+            }

+          }

+        }

+      }

+    }

+  }

+

+

+  method TripleBase(x: int, y: int, z: int)

+    modifies this;

+    requires x < y;

+    requires y < z;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures elems == {x, y, z};

+  {

+    var gensym89 := new SetNode;

+    var gensym90 := new SetNode;

+    gensym89.Init(z);

+    gensym90.Init(x);

+    this.data := y;

+    this.elems := {x, y, z};

+    this.left := gensym90;

+    this.right := gensym89;

+

+    // repr stuff

+    this.Repr := ({this} + this.left.Repr) + this.right.Repr;

+    // assert repr objects are valid (helps verification)

+    assert gensym89.Valid() && gensym90.Valid();

+  }

+

+}

+

+

diff --git a/Source/Jennisys/examples/oopsla12/BHeap.jen b/Source/Jennisys/examples/oopsla12/BHeap.jen
new file mode 100644
index 00000000..41ebec85
--- /dev/null
+++ b/Source/Jennisys/examples/oopsla12/BHeap.jen
@@ -0,0 +1,34 @@
+interface BHeap {

+  var elems: set[int]

+

+  constructor Singleton(x: int)

+    elems := {x}

+

+  constructor Dupleton(a: int, b: int)

+    requires a != b

+    elems := {a b}

+

+  constructor Tripleton(x: int, y: int, z: int)

+    requires x != y && y != z && z != x

+    elems := {x y z}

+

+  method Find(n: int) returns (ret: bool)

+    ret := n in elems

+}

+

+datamodel BHeap {

+  var data: int

+  var left: BHeap

+  var right: BHeap

+

+  frame 

+    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

+    left = null ==> right = null

+    left != null && right = null ==> left.elems = {left.data}

+} 
\ No newline at end of file
diff --git a/Source/Jennisys/examples/oopsla12/BHeap_synth.dfy b/Source/Jennisys/examples/oopsla12/BHeap_synth.dfy
new file mode 100644
index 00000000..addba4ae
--- /dev/null
+++ b/Source/Jennisys/examples/oopsla12/BHeap_synth.dfy
@@ -0,0 +1,220 @@
+class BHeap {

+  ghost var Repr: set<object>;

+  ghost var elems: set<int>;

+

+  var data: int;

+  var left: BHeap;

+  var right: BHeap;

+

+  function Valid_repr(): bool

+    reads *;

+  {

+    this in Repr &&

+    null !in Repr &&

+    (left != null ==> left in Repr && left.Repr <= Repr && this !in left.Repr) &&

+    (right != null ==> right in Repr && right.Repr <= Repr && this !in right.Repr)

+  }

+

+  function Valid_self(): bool

+    reads *;

+  {

+    Valid_repr() &&

+    (elems == ({data} + (if left != null then left.elems else {})) + (if right != null then right.elems else {})) &&

+    (left != null ==> (forall e :: e in left.elems ==> e < data)) &&

+    (right != null ==> (forall e :: e in right.elems ==> e < data)) &&

+    (left == null ==> right == null) &&

+    (left != null && right == null ==> left.elems == {left.data})

+  }

+

+  function Valid(): bool

+    reads *;

+    decreases Repr;

+  {

+    this.Valid_self() &&

+    (left != null ==> left.Valid()) &&

+    (right != null ==> right.Valid()) &&

+    (left != null ==> left.Valid_self()) &&

+    (right != null ==> right.Valid_self()) &&

+    (left != null && left.left != null ==> left.left.Valid_self()) &&

+    (left != null && left.right != null ==> left.right.Valid_self()) &&

+    (right != null && right.left != null ==> right.left.Valid_self()) &&

+    (right != null && right.right != null ==> right.right.Valid_self())

+  }

+

+

+  method Dupleton(a: int, b: int)

+    modifies this;

+    requires a != b;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures elems == {a, b};

+  {

+    if (b < a) {

+      var gensym71 := new BHeap;

+      var gensym73 := new BHeap;

+      this.data := a;

+      this.elems := {b, a};

+      this.left := gensym73;

+      this.right := gensym71;

+      gensym71.data := b;

+      gensym71.elems := {b};

+      gensym71.left := null;

+      gensym71.right := null;

+      gensym73.data := b;

+      gensym73.elems := {b};

+      gensym73.left := null;

+      gensym73.right := null;

+

+      // repr stuff

+      gensym71.Repr := {gensym71};

+      gensym73.Repr := {gensym73};

+      this.Repr := ({this} + {gensym73}) + {gensym71};

+      // assert repr objects are valid (helps verification)

+      assert gensym71.Valid() && gensym73.Valid();

+    } else {

+      var gensym71 := new BHeap;

+      var gensym73 := new BHeap;

+      this.data := b;

+      this.elems := {a, b};

+      this.left := gensym73;

+      this.right := gensym71;

+      gensym71.data := a;

+      gensym71.elems := {a};

+      gensym71.left := null;

+      gensym71.right := null;

+      gensym73.data := a;

+      gensym73.elems := {a};

+      gensym73.left := null;

+      gensym73.right := null;

+

+      // repr stuff

+      gensym71.Repr := {gensym71};

+      gensym73.Repr := {gensym73};

+      this.Repr := ({this} + {gensym73}) + {gensym71};

+      // assert repr objects are valid (helps verification)

+      assert gensym71.Valid() && gensym73.Valid();

+    }

+  }

+

+

+  method Find(n: int) returns (ret: bool)

+    requires Valid();

+    ensures fresh(Repr - old(Repr));

+    ensures Valid();

+    ensures ret == (n in elems);

+    decreases Repr;

+  {

+    if (this.left == null) {

+      ret := n == this.data;

+    } else {

+      if (this.right != null) {

+        var x_10 := this.left.Find(n);

+        var x_11 := this.right.Find(n);

+        ret := (n == this.data || x_10) || x_11;

+      } else {

+        var x_12 := this.left.Find(n);

+        ret := n == this.data || x_12;

+      }

+    }

+  }

+

+

+  method Singleton(x: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures elems == {x};

+  {

+    this.data := x;

+    this.elems := {x};

+    this.left := null;

+    this.right := null;

+

+    // repr stuff

+    this.Repr := {this};

+  }

+

+

+  method Tripleton(x: int, y: int, z: int)

+    modifies this;

+    requires x != y;

+    requires y != z;

+    requires z != x;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures elems == {x, y, z};

+  {

+    if (z < y && x < y) {

+      var gensym75 := new BHeap;

+      var gensym77 := new BHeap;

+      this.data := y;

+      this.elems := {z, x, y};

+      this.left := gensym77;

+      this.right := gensym75;

+      gensym75.data := x;

+      gensym75.elems := {x};

+      gensym75.left := null;

+      gensym75.right := null;

+      gensym77.data := z;

+      gensym77.elems := {z};

+      gensym77.left := null;

+      gensym77.right := null;

+

+      // repr stuff

+      gensym75.Repr := {gensym75};

+      gensym77.Repr := {gensym77};

+      this.Repr := ({this} + {gensym77}) + {gensym75};

+      // assert repr objects are valid (helps verification)

+      assert gensym75.Valid() && gensym77.Valid();

+    } else {

+      if (x < z) {

+        var gensym75 := new BHeap;

+        var gensym77 := new BHeap;

+        this.data := z;

+        this.elems := {x, y, z};

+        this.left := gensym77;

+        this.right := gensym75;

+        gensym75.data := x;

+        gensym75.elems := {x};

+        gensym75.left := null;

+        gensym75.right := null;

+        gensym77.data := y;

+        gensym77.elems := {y};

+        gensym77.left := null;

+        gensym77.right := null;

+

+        // repr stuff

+        gensym75.Repr := {gensym75};

+        gensym77.Repr := {gensym77};

+        this.Repr := ({this} + {gensym77}) + {gensym75};

+        // assert repr objects are valid (helps verification)

+        assert gensym75.Valid() && gensym77.Valid();

+      } else {

+        var gensym75 := new BHeap;

+        var gensym77 := new BHeap;

+        this.data := x;

+        this.elems := {z, y, x};

+        this.left := gensym77;

+        this.right := gensym75;

+        gensym75.data := y;

+        gensym75.elems := {y};

+        gensym75.left := null;

+        gensym75.right := null;

+        gensym77.data := z;

+        gensym77.elems := {z};

+        gensym77.left := null;

+        gensym77.right := null;

+

+        // repr stuff

+        gensym75.Repr := {gensym75};

+        gensym77.Repr := {gensym77};

+        this.Repr := ({this} + {gensym77}) + {gensym75};

+        // assert repr objects are valid (helps verification)

+        assert gensym75.Valid() && gensym77.Valid();

+      }

+    }

+  }

+

+}

+

+

diff --git a/Source/Jennisys/examples/oopsla12/DList.jen b/Source/Jennisys/examples/oopsla12/DList.jen
new file mode 100644
index 00000000..7e087f95
--- /dev/null
+++ b/Source/Jennisys/examples/oopsla12/DList.jen
@@ -0,0 +1,40 @@
+interface DList[T] {

+  var list: seq[T]

+

+  invariant

+    |list| > 0

+

+  constructor Init(t: T)

+    list := [t]

+

+  constructor Double(p: T, q: T)

+    list := [p q]

+

+  method List() returns (ret: seq[T])

+    ret := list

+

+  method Size() returns (ret: int)

+    ret := |list|

+

+  method Get(idx: int) returns (ret: T)

+    requires 0 <= idx && idx < |list|

+    ret := list[idx]

+

+  method Find(n: T) returns (ret: bool)

+    ret := n in list

+}

+

+datamodel DList[T] {

+  var data: T

+  var next: DList[T]

+  var prev: DList[T]

+

+  frame

+    next

+

+  invariant

+    next = null ==> list = [data]

+    next != null ==> (list = [data] + next.list  

+                      &&  next.prev = this)

+    prev != null ==> prev.next = this

+}
\ No newline at end of file
diff --git a/Source/Jennisys/examples/oopsla12/DList_synth.dfy b/Source/Jennisys/examples/oopsla12/DList_synth.dfy
new file mode 100644
index 00000000..897a6de0
--- /dev/null
+++ b/Source/Jennisys/examples/oopsla12/DList_synth.dfy
@@ -0,0 +1,154 @@
+class DList<T> {

+  ghost var Repr: set<object>;

+  ghost var list: seq<T>;

+

+  var data: T;

+  var next: DList<T>;

+  var prev: DList<T>;

+

+  function Valid_repr(): bool

+    reads *;

+  {

+    this in Repr &&

+    null !in Repr &&

+    (next != null ==> next in Repr && next.Repr <= Repr && this !in next.Repr)

+  }

+

+  function Valid_self(): bool

+    reads *;

+  {

+    Valid_repr() &&

+    (next == null ==> (list == [data] && list[0] == data) && |list| == 1) &&

+    (next != null ==> list == [data] + next.list && next.prev == this) &&

+    (prev != null ==> prev.next == this) &&

+    (|list| > 0)

+  }

+

+  function Valid(): bool

+    reads *;

+    decreases Repr;

+  {

+    this.Valid_self() &&

+    (next != null ==> next.Valid()) &&

+    (next != null ==> next.Valid_self()) &&

+    (next != null && next.next != null ==> next.next.Valid_self())

+  }

+

+

+  method Double(p: T, q: T)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures list == [p, q];

+    ensures list[0] == p;

+    ensures list[1] == q;

+    ensures |list| == 2;

+  {

+    var gensym71 := new DList<T>;

+    this.data := p;

+    this.list := [p, q];

+    this.next := gensym71;

+    this.prev := null;

+    gensym71.data := q;

+    gensym71.list := [q];

+    gensym71.next := null;

+    gensym71.prev := this;

+

+    // repr stuff

+    this.Repr := {this} + {gensym71};

+    gensym71.Repr := {gensym71};

+    // assert repr objects are valid (helps verification)

+    assert gensym71.Valid();

+  }

+

+

+  method Find(n: T) returns (ret: bool)

+    requires Valid();

+    ensures fresh(Repr - old(Repr));

+    ensures Valid();

+    ensures ret == (n in list);

+    decreases Repr;

+  {

+    if (this.next == null) {

+      ret := n == this.data;

+    } else {

+      var x_5 := this.next.Find(n);

+      ret := n == this.data || x_5;

+    }

+  }

+

+

+  method Get(idx: int) returns (ret: T)

+    requires Valid();

+    requires 0 <= idx;

+    requires idx < |list|;

+    ensures fresh(Repr - old(Repr));

+    ensures Valid();

+    ensures ret == list[idx];

+    decreases Repr;

+  {

+    if (this.next == null) {

+      ret := this.data;

+    } else {

+      if (idx == 0) {

+        ret := this.data;

+      } else {

+        var x_6 := this.next.Get(idx - 1);

+        ret := x_6;

+      }

+    }

+  }

+

+

+  method Init(t: T)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures list == [t];

+    ensures list[0] == t;

+    ensures |list| == 1;

+  {

+    this.data := t;

+    this.list := [t];

+    this.next := null;

+    this.prev := null;

+

+    // repr stuff

+    this.Repr := {this};

+  }

+

+

+  method List() returns (ret: seq<T>)

+    requires Valid();

+    ensures fresh(Repr - old(Repr));

+    ensures Valid();

+    ensures ret == list;

+    decreases Repr;

+  {

+    if (this.next == null) {

+      ret := [this.data];

+    } else {

+      var x_7 := this.next.List();

+      ret := [this.data] + x_7;

+    }

+  }

+

+

+  method Size() returns (ret: int)

+    requires Valid();

+    ensures fresh(Repr - old(Repr));

+    ensures Valid();

+    ensures ret == |list|;

+    decreases Repr;

+  {

+    if (this.next == null) {

+      ret := 1;

+    } else {

+      var x_8 := this.next.Size();

+      ret := 1 + x_8;

+    }

+  }

+

+}

+

+

diff --git a/Source/Jennisys/examples/oopsla12/IntSet.jen b/Source/Jennisys/examples/oopsla12/IntSet.jen
new file mode 100644
index 00000000..4800371e
--- /dev/null
+++ b/Source/Jennisys/examples/oopsla12/IntSet.jen
@@ -0,0 +1,30 @@
+interface IntSet {

+  var elems: set[int]             

+

+  constructor Singleton(x: int)

+    elems := {x}

+

+  constructor Dupleton(x: int, y: int)

+    requires x != y

+    elems := {x y}

+

+  method Find(x: int) returns (ret: bool)

+    ret := x in elems

+}

+

+datamodel IntSet {

+  var data: int

+  var left: IntSet

+  var right: IntSet

+  

+  frame 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 ==> data < e)

+} 
\ No newline at end of file
diff --git a/Source/Jennisys/examples/oopsla12/IntSet_synth.dfy b/Source/Jennisys/examples/oopsla12/IntSet_synth.dfy
new file mode 100644
index 00000000..55523e79
--- /dev/null
+++ b/Source/Jennisys/examples/oopsla12/IntSet_synth.dfy
@@ -0,0 +1,130 @@
+class IntSet {

+  ghost var Repr: set<object>;

+  ghost var elems: set<int>;

+

+  var data: int;

+  var left: IntSet;

+  var right: IntSet;

+

+  function Valid_repr(): bool

+    reads *;

+  {

+    this in Repr &&

+    null !in Repr &&

+    (left != null ==> left in Repr && left.Repr <= Repr && this !in left.Repr) &&

+    (right != null ==> right in Repr && right.Repr <= Repr && this !in right.Repr)

+  }

+

+  function Valid_self(): bool

+    reads *;

+  {

+    Valid_repr() &&

+    (elems == ({data} + (if left != null then left.elems else {})) + (if right != null then right.elems else {})) &&

+    (left != null ==> (forall e :: e in left.elems ==> e < data)) &&

+    (right != null ==> (forall e :: e in right.elems ==> data < e))

+  }

+

+  function Valid(): bool

+    reads *;

+    decreases Repr;

+  {

+    this.Valid_self() &&

+    (left != null ==> left.Valid()) &&

+    (right != null ==> right.Valid()) &&

+    (left != null ==> left.Valid_self()) &&

+    (right != null ==> right.Valid_self()) &&

+    (left != null && left.left != null ==> left.left.Valid_self()) &&

+    (left != null && left.right != null ==> left.right.Valid_self()) &&

+    (right != null && right.left != null ==> right.left.Valid_self()) &&

+    (right != null && right.right != null ==> right.right.Valid_self())

+  }

+

+

+  method Dupleton(x: int, y: int)

+    modifies this;

+    requires x != y;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures elems == {x, y};

+  {

+    if (x < y) {

+      var gensym73 := new IntSet;

+      this.data := x;

+      this.elems := {x, y};

+      this.left := null;

+      this.right := gensym73;

+      gensym73.data := y;

+      gensym73.elems := {y};

+      gensym73.left := null;

+      gensym73.right := null;

+

+      // repr stuff

+      gensym73.Repr := {gensym73};

+      this.Repr := {this} + {gensym73};

+      // assert repr objects are valid (helps verification)

+      assert gensym73.Valid();

+    } else {

+      var gensym73 := new IntSet;

+      this.data := y;

+      this.elems := {y, x};

+      this.left := null;

+      this.right := gensym73;

+      gensym73.data := x;

+      gensym73.elems := {x};

+      gensym73.left := null;

+      gensym73.right := null;

+

+      // repr stuff

+      gensym73.Repr := {gensym73};

+      this.Repr := {this} + {gensym73};

+      // assert repr objects are valid (helps verification)

+      assert gensym73.Valid();

+    }

+  }

+

+

+  method Find(x: int) returns (ret: bool)

+    requires Valid();

+    ensures fresh(Repr - old(Repr));

+    ensures Valid();

+    ensures ret == (x in elems);

+    decreases Repr;

+  {

+    if (this.left != null && this.right != null) {

+      var x_13 := this.left.Find(x);

+      var x_14 := this.right.Find(x);

+      ret := (x == this.data || x_13) || x_14;

+    } else {

+      if (this.left != null) {

+        var x_15 := this.left.Find(x);

+        ret := x == this.data || x_15;

+      } else {

+        if (this.right != null) {

+          var x_16 := this.right.Find(x);

+          ret := x == this.data || x_16;

+        } else {

+          ret := x == this.data;

+        }

+      }

+    }

+  }

+

+

+  method Singleton(x: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures elems == {x};

+  {

+    this.data := x;

+    this.elems := {x};

+    this.left := null;

+    this.right := null;

+

+    // repr stuff

+    this.Repr := {this};

+  }

+

+}

+

+

diff --git a/Source/Jennisys/examples/oopsla12/List.jen b/Source/Jennisys/examples/oopsla12/List.jen
new file mode 100644
index 00000000..10a70050
--- /dev/null
+++ b/Source/Jennisys/examples/oopsla12/List.jen
@@ -0,0 +1,29 @@
+interface List[T] {

+  var list: seq[T]

+  invariant |list| > 0

+

+  constructor Singleton(t: T)

+    list := [t]

+  constructor Dupleton(p: T, q: T)

+    list := [p q]

+  method Elems() returns (ret: seq[T])

+    ret := list

+  method Get(idx: int) returns (ret: T)

+    requires 0 <= idx && idx < |list|

+    ret := list[idx]

+  method Find(n: T) returns (ret: bool)

+    ret := n in list

+  method Size() returns (ret: int)

+    ret := |list|

+}

+    

+datamodel List[T] {    

+  var data: T

+  var next: List[T]

+

+  frame next

+  

+  invariant

+    next = null  ==> list = [data]

+    next != null ==> list = [data] + next.list

+}
\ No newline at end of file
diff --git a/Source/Jennisys/examples/oopsla12/List_synth.dfy b/Source/Jennisys/examples/oopsla12/List_synth.dfy
new file mode 100644
index 00000000..5cbfa10e
--- /dev/null
+++ b/Source/Jennisys/examples/oopsla12/List_synth.dfy
@@ -0,0 +1,146 @@
+class List<T> {

+  ghost var Repr: set<object>;

+  ghost var list: seq<T>;

+

+  var data: T;

+  var next: List<T>;

+

+  function Valid_repr(): bool

+    reads *;

+  {

+    this in Repr &&

+    null !in Repr &&

+    (next != null ==> next in Repr && next.Repr <= Repr && this !in next.Repr)

+  }

+

+  function Valid_self(): bool

+    reads *;

+  {

+    Valid_repr() &&

+    (next == null ==> (list == [data] && list[0] == data) && |list| == 1) &&

+    (next != null ==> list == [data] + next.list) &&

+    (|list| > 0)

+  }

+

+  function Valid(): bool

+    reads *;

+    decreases Repr;

+  {

+    this.Valid_self() &&

+    (next != null ==> next.Valid()) &&

+    (next != null ==> next.Valid_self()) &&

+    (next != null && next.next != null ==> next.next.Valid_self())

+  }

+

+

+  method Dupleton(p: T, q: T)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures list == [p, q];

+    ensures list[0] == p;

+    ensures list[1] == q;

+    ensures |list| == 2;

+  {

+    var gensym71 := new List<T>;

+    gensym71.Singleton(q);

+    this.data := p;

+    this.list := [p, q];

+    this.next := gensym71;

+

+    // repr stuff

+    this.Repr := {this} + this.next.Repr;

+    // assert repr objects are valid (helps verification)

+    assert gensym71.Valid();

+  }

+

+

+  method Elems() returns (ret: seq<T>)

+    requires Valid();

+    ensures fresh(Repr - old(Repr));

+    ensures Valid();

+    ensures ret == list;

+    decreases Repr;

+  {

+    if (this.next == null) {

+      ret := [this.data];

+    } else {

+      var x_5 := this.next.Elems();

+      ret := [this.data] + x_5;

+    }

+  }

+

+

+  method Find(n: T) returns (ret: bool)

+    requires Valid();

+    ensures fresh(Repr - old(Repr));

+    ensures Valid();

+    ensures ret == (n in list);

+    decreases Repr;

+  {

+    if (this.next == null) {

+      ret := n == this.data;

+    } else {

+      var x_6 := this.next.Find(n);

+      ret := n == this.data || x_6;

+    }

+  }

+

+

+  method Get(idx: int) returns (ret: T)

+    requires Valid();

+    requires 0 <= idx;

+    requires idx < |list|;

+    ensures fresh(Repr - old(Repr));

+    ensures Valid();

+    ensures ret == list[idx];

+    decreases Repr;

+  {

+    if (this.next == null) {

+      ret := this.data;

+    } else {

+      if (idx == 0) {

+        ret := this.data;

+      } else {

+        var x_7 := this.next.Get(idx - 1);

+        ret := x_7;

+      }

+    }

+  }

+

+

+  method Singleton(t: T)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures list == [t];

+    ensures list[0] == t;

+    ensures |list| == 1;

+  {

+    this.data := t;

+    this.list := [t];

+    this.next := null;

+

+    // repr stuff

+    this.Repr := {this};

+  }

+

+

+  method Size() returns (ret: int)

+    requires Valid();

+    ensures fresh(Repr - old(Repr));

+    ensures Valid();

+    ensures ret == |list|;

+    decreases Repr;

+  {

+    if (this.next == null) {

+      ret := 1;

+    } else {

+      var x_8 := this.next.Size();

+      ret := 1 + x_8;

+    }

+  }

+

+}

+

+

diff --git a/Source/Jennisys/examples/oopsla12/Math.jen b/Source/Jennisys/examples/oopsla12/Math.jen
new file mode 100644
index 00000000..0cc772b3
--- /dev/null
+++ b/Source/Jennisys/examples/oopsla12/Math.jen
@@ -0,0 +1,20 @@
+interface Math {

+  method Min2(a: int, b: int) returns (ret: int)

+    ensures a < b ==> ret = a

+    ensures a >= b ==> ret = b

+

+  method Min3Sum(a: int, b: int, c: int) 

+      returns (ret: int)

+    ensures ret in {a+b a+c b+c}

+    ensures forall x :: x in {a+b a+c b+c} ==> ret <= x

+

+  method Min4(a: int, b: int, c: int, d: int) 

+      returns (ret: int)

+    ensures ret in {a b c d}

+    ensures forall x :: x in {a b c d} ==> ret <= x

+

+  method Abs(a: int) returns (ret: int)

+    ensures ret in {a (-a)} && ret >= 0

+}

+

+datamodel Math {}
\ No newline at end of file
diff --git a/Source/Jennisys/examples/oopsla12/Math_synth.dfy b/Source/Jennisys/examples/oopsla12/Math_synth.dfy
new file mode 100644
index 00000000..68893b3d
--- /dev/null
+++ b/Source/Jennisys/examples/oopsla12/Math_synth.dfy
@@ -0,0 +1,105 @@
+class Math {

+  ghost var Repr: set<object>;

+

+

+  function Valid_repr(): bool

+    reads *;

+  {

+    this in Repr &&

+    null !in Repr

+  }

+

+  function Valid_self(): bool

+    reads *;

+  {

+    Valid_repr() &&

+    true

+  }

+

+  function Valid(): bool

+    reads *;

+  {

+    this.Valid_self() &&

+    true

+  }

+

+

+  method Abs(a: int) returns (ret: int)

+    requires Valid();

+    ensures fresh(Repr - old(Repr));

+    ensures Valid();

+    ensures ret in {a, -a};

+    ensures ret >= 0;

+  {

+    if (a >= 0) {

+      ret := a;

+    } else {

+      ret := -a;

+    }

+  }

+

+

+  method Min2(a: int, b: int) returns (ret: int)

+    requires Valid();

+    ensures fresh(Repr - old(Repr));

+    ensures Valid();

+    ensures a < b ==> ret == a;

+    ensures a >= b ==> ret == b;

+  {

+    if (a < b) {

+      ret := a;

+    } else {

+      ret := b;

+    }

+  }

+

+

+  method Min3Sum(a: int, b: int, c: int) returns (ret: int)

+    requires Valid();

+    ensures fresh(Repr - old(Repr));

+    ensures Valid();

+    ensures ret in {a + b, a + c, b + c};

+    ensures ret <= a + b;

+    ensures ret <= a + c;

+    ensures ret <= b + c;

+  {

+    if (a + b <= a + c && a + b <= b + c) {

+      ret := a + b;

+    } else {

+      if (b + c <= a + c) {

+        ret := b + c;

+      } else {

+        ret := a + c;

+      }

+    }

+  }

+

+

+  method Min4(a: int, b: int, c: int, d: int) returns (ret: int)

+    requires Valid();

+    ensures fresh(Repr - old(Repr));

+    ensures Valid();

+    ensures ret in {a, b, c, d};

+    ensures ret <= a;

+    ensures ret <= b;

+    ensures ret <= c;

+    ensures ret <= d;

+  {

+    if ((a <= b && a <= c) && a <= d) {

+      ret := a;

+    } else {

+      if (d <= b && d <= c) {

+        ret := d;

+      } else {

+        if (c <= b) {

+          ret := c;

+        } else {

+          ret := b;

+        }

+      }

+    }

+  }

+

+}

+

+

diff --git a/Source/Jennisys/examples/set.dfy b/Source/Jennisys/examples/set.dfy
new file mode 100644
index 00000000..627f1ecb
--- /dev/null
+++ b/Source/Jennisys/examples/set.dfy
@@ -0,0 +1,246 @@
+class Set {

+  ghost var Repr: set<object>;

+  ghost var elems: set<int>;

+

+  var root: SetNode;

+

+  function Valid_repr(): bool

+    reads *;

+  {

+    this in Repr &&

+    null !in Repr &&

+    (root != null ==> root in Repr && root.Repr <= Repr && this !in root.Repr)

+  }

+

+  function Valid_self(): bool

+    reads *;

+  {

+    Valid_repr() &&

+    (root == null ==> elems == {}) &&

+    (root != null ==> elems == root.elems)

+  }

+

+  function Valid(): bool

+    reads *;

+  {

+    this.Valid_self() &&

+    (root != null ==> root.Valid())

+  }

+

+  method Empty()

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures elems == {};

+  {

+    this.elems := {};

+    this.root := null;

+    // repr stuff

+    this.Repr := {this};

+  }

+

+  method Singleton(t: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures elems == {t};

+  {

+    var gensym66 := new SetNode;

+    gensym66.Init(t);

+    this.elems := {t};

+    this.root := gensym66;

+    this.Repr := {this} + this.root.Repr;

+  }

+

+  method Sum(p: int, q: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures elems == {p + q};

+  {

+    var gensym68 := new SetNode;

+    gensym68.Init(p+q);

+    this.elems := {p + q};

+    this.root := gensym68;

+    this.Repr := {this} + this.root.Repr;

+  }

+

+  method Double(p: int, q: int)

+    modifies this;

+    requires p != q;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures elems == {p, q};

+  {

+    var gensym71 := new SetNode; 

+    gensym71.Double(p, q);

+    this.elems := {p, q}; 

+    this.root := gensym71; 

+    this.Repr := {this} + this.root.Repr; 

+  }

+

+}

+

+class SetNode {

+  ghost var Repr: set<object>;

+  ghost var elems: set<int>;

+

+  var data: int;

+  var left: SetNode;

+  var right: SetNode;

+

+  function Valid_repr(): bool

+    reads *;

+  {

+    this in Repr &&

+    null !in Repr &&

+    (left != null ==> left in Repr && left.Repr <= Repr && this !in left.Repr) &&

+    (right != null ==> right in Repr && right.Repr <= Repr && this !in right.Repr)

+  }

+

+  function Valid_self(): bool

+    reads *;

+  {

+    Valid_repr() &&

+    (elems == ({data} + (if left != null then left.elems else {})) + (if right != null then right.elems else {})) &&

+    (left != null ==> (forall e :: e in left.elems ==> e < data)) &&

+    (right != null ==> (forall e :: e in right.elems ==> e > data))

+  }

+

+  function Valid(): bool

+    reads *;

+  {

+    this.Valid_self() &&

+    (left != null ==> left.Valid_self() && (left.left != null ==> left.left.Valid_self())) &&

+    (right != null ==> right.Valid_self() && (right.right != null ==> right.right.Valid_self()))

+  }

+

+  method Init(t: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures elems == {t};

+  {

+    this.data := t;

+    this.elems := {t};

+    this.left := null;

+    this.right := null;

+    // repr stuff

+    this.Repr := {this};

+  }

+

+  method Double(p: int, q: int)

+    modifies this;

+//    requires p != q;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures elems == {p, q};

+  {

+    if (q > p) {

+      var gensym79 := new SetNode;

+      gensym79.Init(q);

+      this.data := p;

+      this.elems := {p, q};

+      this.left := null;

+      this.right := gensym79;

+      this.Repr := {this} + this.right.Repr;

+    } else if (q < p) {

+      var gensym79 := new SetNode;

+      gensym79.Init(p);

+      this.data := q;

+      this.elems := {p, q};

+      this.left := null;

+      this.right := gensym79;

+      this.Repr := {this} + this.right.Repr;

+    } else {

+      this.data := p; 

+      this.elems := {p};

+      this.left := null;

+      this.right := null;

+      this.Repr := {this};

+    } 

+  }

+

+  method Triple(p: int, q: int, r: int)

+    modifies this;

+    requires p != q;

+    requires q != r;

+    requires r != p;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures elems == {p, q, r};

+  {

+    if (p < q && r > q) {

+      var gensym83 := new SetNode;

+      var gensym84 := new SetNode;

+      gensym83.Init(r);

+      gensym84.Init(p);

+      this.data := q;

+      this.elems := {p, q, r};

+      this.left := gensym84;

+      this.right := gensym83;

+      this.Repr := ({this} + this.left.Repr) + this.right.Repr;

+    } else {

+      if (p < r && q > r) {

+        var gensym85 := new SetNode;

+        var gensym86 := new SetNode;

+        gensym85.Init(q);

+        gensym86.Init(p);

+        this.data := r;

+        this.elems := {p, q, r};

+        this.left := gensym86;

+        this.right := gensym85;

+        this.Repr := ({this} + this.left.Repr) + this.right.Repr;

+      } else {

+        if (r < p && q > p) {

+          var gensym84 := new SetNode;

+          var gensym85 := new SetNode;

+          gensym84.Init(q);

+          gensym85.Init(r);

+          this.data := p;

+          this.elems := {p, q, r};

+          this.left := gensym85;

+          this.right := gensym84;

+          this.Repr := ({this} + this.left.Repr) + this.right.Repr;

+        } else {

+          if (q < p && r > p) {

+            var gensym82 := new SetNode;

+            var gensym83 := new SetNode;

+            gensym82.Init(r);

+            gensym83.Init(q);

+            this.data := p;

+            this.elems := {p, q, r};

+            this.left := gensym83;

+            this.right := gensym82;

+            this.Repr := ({this} + this.left.Repr) + this.right.Repr;

+          } else {

+            if (q < r && p > r) {

+              var gensym85 := new SetNode;

+              var gensym86 := new SetNode;

+              gensym85.Init(p);

+              gensym86.Init(q);

+              this.data := r;

+              this.elems := {p, q, r};

+              this.left := gensym86;

+              this.right := gensym85;

+              this.Repr := ({this} + this.left.Repr) + this.right.Repr;

+            } else {

+              var gensym82 := new SetNode;

+              var gensym83 := new SetNode;

+              gensym82.Init(p);

+              gensym83.Init(r);

+              this.data := q;

+              this.elems := {p, q, r};

+              this.left := gensym83;

+              this.right := gensym82;

+              this.Repr := ({this} + this.left.Repr) + this.right.Repr;

+            }

+          }

+        }

+      }

+    }

+  }

+

+}

+

+