Jennisys: started to work on synthesizing some methods. So far, only

  infrastructural things have been implemented, like handling return parameters,
  generating different "fresh" spec for methods than for constructors,
  adding "Valid()" to method preconditions.

9 files changed, 361 insertions, 238 deletions

diff --git a/Jennisys/examples/List.jen b/Jennisys/examples/List.jen
index 63535a20..a7ba26ed 100644
--- a/Jennisys/examples/List.jen
+++ b/Jennisys/examples/List.jen
@@ -33,6 +33,10 @@ class Node[T] {
 
   constructor Double(p: T, q: T)
     ensures list = [p q]
+
+  method List() returns (lst: seq[T])
+    requires |list| = 1
+    ensures lst = list
 }
 
 model Node[T] {
diff --git a/Jennisys/examples/NumberMethods.jen b/Jennisys/examples/NumberMethods.jen
new file mode 100644
index 00000000..91fbc4f9
--- /dev/null
+++ b/Jennisys/examples/NumberMethods.jen
@@ -0,0 +1,40 @@
+class 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
+
+}
+
+model NumberMethods {
+
+}
\ No newline at end of file
diff --git a/Jennisys/examples/Set.jen b/Jennisys/examples/Set.jen
index b867a007..0bd42701 100644
--- a/Jennisys/examples/Set.jen
+++ b/Jennisys/examples/Set.jen
@@ -14,9 +14,6 @@ class Set {
     requires p != q
     ensures elems = {p q}
 
-  constructor Triple(p: int, q: int, r: int)
-    requires p != q && q != r && r != p
-    ensures elems = {p q r}
 }
 
 model Set {
@@ -36,9 +33,9 @@ class SetNode {
   constructor Init(x: int)
     ensures elems = {x}
 
-  constructor Double(x: int, y: int)
-    requires x != y
-    ensures elems = {x y}
+  constructor Double(a: int, b: int)
+    requires a != b
+    ensures elems = {a b}
 
   constructor DoubleBase(x: int, y: int)
     requires x > y
diff --git a/Jennisys/examples/mod2/jennisys-synth_List.dfy b/Jennisys/examples/mod2/jennisys-synth_List.dfy
index e3f7a701..a87d9b50 100644
--- a/Jennisys/examples/mod2/jennisys-synth_List.dfy
+++ b/Jennisys/examples/mod2/jennisys-synth_List.dfy
@@ -33,6 +33,9 @@ class List<T> {
     ensures fresh(Repr - {this});

     ensures Valid();

     ensures list == [p, q];

+    ensures list[0] == p;

+    ensures list[1] == q;

+    ensures |list| == 2;

   {

     var gensym68 := new Node<T>;

     gensym68.Double(p, q);

@@ -48,6 +51,7 @@ class List<T> {
     ensures fresh(Repr - {this});

     ensures Valid();

     ensures list == [];

+    ensures |list| == 0;

   {

     this.list := [];

     this.root := null;

@@ -61,6 +65,8 @@ class List<T> {
     ensures fresh(Repr - {this});

     ensures Valid();

     ensures list == [t];

+    ensures list[0] == t;

+    ensures |list| == 1;

   {

     var gensym67 := new Node<T>;

     gensym67.Init(t);

@@ -110,6 +116,9 @@ class Node<T> {
     ensures fresh(Repr - {this});

     ensures Valid();

     ensures list == [p, q];

+    ensures list[0] == p;

+    ensures list[1] == q;

+    ensures |list| == 2;

   {

     var gensym74 := new Node<T>;

     gensym74.Init(q);

@@ -126,6 +135,8 @@ class Node<T> {
     ensures fresh(Repr - {this});

     ensures Valid();

     ensures list == [t];

+    ensures list[0] == t;

+    ensures |list| == 1;

   {

     this.data := t;

     this.list := [t];

diff --git a/Jennisys/examples/mod2/jennisys-synth_List2.dfy b/Jennisys/examples/mod2/jennisys-synth_List2.dfy
index 08268640..27c2d3b3 100644
--- a/Jennisys/examples/mod2/jennisys-synth_List2.dfy
+++ b/Jennisys/examples/mod2/jennisys-synth_List2.dfy
@@ -33,6 +33,9 @@ class IntList {
     ensures fresh(Repr - {this});

     ensures Valid();

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

+    ensures list[0] == p;

+    ensures list[1] == q;

+    ensures |list| == 2;

   {

     var gensym67 := new IntNode;

     gensym67.Double(p, q);

@@ -48,6 +51,7 @@ class IntList {
     ensures fresh(Repr - {this});

     ensures Valid();

     ensures list == [];

+    ensures |list| == 0;

   {

     this.list := [];

     this.root := null;

@@ -61,13 +65,11 @@ class IntList {
     ensures fresh(Repr - {this});

     ensures Valid();

     ensures list == [1, 2];

+    ensures list[0] == 1;

+    ensures list[1] == 2;

+    ensures |list| == 2;

   {

-    var gensym65 := new IntNode;

-    gensym65.Double(1, 2);

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

-    this.root := gensym65;

-    // repr stuff

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

+    this.Double(1, 2);

   }

 

 

@@ -76,6 +78,8 @@ class IntList {
     ensures fresh(Repr - {this});

     ensures Valid();

     ensures list == [p];

+    ensures list[0] == p;

+    ensures |list| == 1;

   {

     var gensym66 := new IntNode;

     gensym66.Init(p);

@@ -91,13 +95,10 @@ class IntList {
     ensures fresh(Repr - {this});

     ensures Valid();

     ensures list == [2];

+    ensures list[0] == 2;

+    ensures |list| == 1;

   {

-    var gensym65 := new IntNode;

-    gensym65.Init(2);

-    this.list := [2];

-    this.root := gensym65;

-    // repr stuff

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

+    this.Singleton(2);

   }

 

 

@@ -106,13 +107,10 @@ class IntList {
     ensures fresh(Repr - {this});

     ensures Valid();

     ensures list == [p + q];

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

+    ensures |list| == 1;

   {

-    var gensym67 := new IntNode;

-    gensym67.Init(p + q);

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

-    this.root := gensym67;

-    // repr stuff

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

+    this.Singleton(p + q);

   }

 

 

@@ -121,13 +119,11 @@ class IntList {
     ensures fresh(Repr - {this});

     ensures Valid();

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

+    ensures list[0] == p;

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

+    ensures |list| == 2;

   {

-    var gensym66 := new IntNode;

-    gensym66.Double(p, p + 1);

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

-    this.root := gensym66;

-    // repr stuff

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

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

   }

 

 }

@@ -165,25 +161,14 @@ class IntNode {
   }

 

 

-  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 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 gensym74 := new IntNode;

     gensym74.Init(y);

@@ -200,6 +185,8 @@ class IntNode {
     ensures fresh(Repr - {this});

     ensures Valid();

     ensures list == [x];

+    ensures list[0] == x;

+    ensures |list| == 1;

   {

     this.data := x;

     this.list := [x];

@@ -208,6 +195,18 @@ class IntNode {
     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/Jennisys/examples/mod2/jennisys-synth_List3.dfy b/Jennisys/examples/mod2/jennisys-synth_List3.dfy
index 9eba9fe6..56fa4b7b 100644
--- a/Jennisys/examples/mod2/jennisys-synth_List3.dfy
+++ b/Jennisys/examples/mod2/jennisys-synth_List3.dfy
@@ -33,6 +33,9 @@ class IntList {
     ensures fresh(Repr - {this});

     ensures Valid();

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

+    ensures list[0] == p;

+    ensures list[1] == q;

+    ensures |list| == 2;

   {

     var gensym68 := new IntNode;

     gensym68._synth_IntList_Double_gensym68(p, q);

@@ -48,6 +51,7 @@ class IntList {
     ensures fresh(Repr - {this});

     ensures Valid();

     ensures list == [];

+    ensures |list| == 0;

   {

     this.list := [];

     this.root := null;

@@ -61,13 +65,11 @@ class IntList {
     ensures fresh(Repr - {this});

     ensures Valid();

     ensures list == [1, 2];

+    ensures list[0] == 1;

+    ensures list[1] == 2;

+    ensures |list| == 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;

+    this.Double(1, 2);

   }

 

 

@@ -76,6 +78,8 @@ class IntList {
     ensures fresh(Repr - {this});

     ensures Valid();

     ensures list == [p];

+    ensures list[0] == p;

+    ensures |list| == 1;

   {

     var gensym67 := new IntNode;

     gensym67._synth_IntList_Singleton_gensym67(p);

@@ -91,13 +95,10 @@ class IntList {
     ensures fresh(Repr - {this});

     ensures Valid();

     ensures list == [2];

+    ensures list[0] == 2;

+    ensures |list| == 1;

   {

-    var gensym66 := new IntNode;

-    gensym66._synth_IntList_SingletonTwo_gensym66();

-    this.list := [2];

-    this.root := gensym66;

-    // repr stuff

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

+    this.Singleton(2);

   }

 

 

@@ -106,13 +107,10 @@ class IntList {
     ensures fresh(Repr - {this});

     ensures Valid();

     ensures list == [p + q];

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

+    ensures |list| == 1;

   {

-    var gensym68 := new IntNode;

-    gensym68._synth_IntList_Sum_gensym68(p, q);

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

-    this.root := gensym68;

-    // repr stuff

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

+    this.Singleton(p + q);

   }

 

 

@@ -121,13 +119,11 @@ class IntList {
     ensures fresh(Repr - {this});

     ensures Valid();

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

+    ensures list[0] == p;

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

+    ensures |list| == 2;

   {

-    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;

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

   }

 

 }

@@ -185,11 +181,26 @@ class IntNode {
     ensures Valid();

     ensures data == p + 1;

   {

-    this.data := p + 1;

-    this.next := null;

-    this.succ := [];

+    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 gensym73 := new IntNode;

+    gensym73._synth_IntNode_OneTwo_gensym73();

+    this.data := 1;

+    this.next := gensym73;

+    this.succ := [gensym73];

     // repr stuff

-    this.Repr := {this};

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

   }

 

 

@@ -199,6 +210,7 @@ class IntNode {
     ensures Valid();

     ensures data == 0;

     ensures succ == [];

+    ensures |succ| == 0;

   {

     this.data := 0;

     this.next := null;

@@ -216,6 +228,7 @@ class IntNode {
     ensures |succ| == 1;

     ensures succ[0].data == q;

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

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

   {

     var gensym80 := new IntNode;

     gensym80._synth_IntNode__synth_IntList_Double_gensym68_gensym80(q);

@@ -227,40 +240,6 @@ class IntNode {
   }

 

 

-  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_gensym66()

-    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_gensym67(p: int)

     modifies this;

     ensures fresh(Repr - {this});

@@ -276,59 +255,6 @@ class IntNode {
   }

 

 

-  method _synth_IntList_Sum_gensym68(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});

@@ -358,36 +284,6 @@ class IntNode {
     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/Jennisys/examples/mod2/jennisys-synth_Number.dfy b/Jennisys/examples/mod2/jennisys-synth_Number.dfy
index 454a8548..0b5504d2 100644
--- a/Jennisys/examples/mod2/jennisys-synth_Number.dfy
+++ b/Jennisys/examples/mod2/jennisys-synth_Number.dfy
@@ -162,7 +162,7 @@ class Number {
     ensures num <= b + c;

     ensures num <= a + c;

   {

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

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

   }

 

 

diff --git a/Jennisys/examples/mod2/jennisys-synth_NumberMethods.dfy b/Jennisys/examples/mod2/jennisys-synth_NumberMethods.dfy
new file mode 100644
index 00000000..7e6c68e4
--- /dev/null
+++ b/Jennisys/examples/mod2/jennisys-synth_NumberMethods.dfy
@@ -0,0 +1,176 @@
+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)

+    modifies this;

+    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)

+    modifies this;

+    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)

+    modifies this;

+    requires Valid();

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

+    ensures Valid();

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

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

+  {

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

+      ret := a;

+    } else {

+      ret := b;

+    }

+  }

+

+

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

+    modifies this;

+    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)

+    modifies this;

+    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)

+    modifies this;

+    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)

+    modifies this;

+    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)

+    modifies this;

+    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)

+    modifies this;

+    requires Valid();

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

+    ensures Valid();

+    ensures ret == a + b;

+  {

+    ret := a + b;

+  }

+

+}

+

+

diff --git a/Jennisys/examples/mod2/jennisys-synth_Set.dfy b/Jennisys/examples/mod2/jennisys-synth_Set.dfy
index 8449b03c..a3407cc8 100644
--- a/Jennisys/examples/mod2/jennisys-synth_Set.dfy
+++ b/Jennisys/examples/mod2/jennisys-synth_Set.dfy
@@ -122,6 +122,54 @@ class SetNode {
   }

 

 

+  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 {

+      this.DoubleBase(a, b);

+    }

+  }

+

+

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

+    modifies this;

+    requires x > y;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures elems == {x, y};

+  {

+    var gensym77 := new SetNode;

+    gensym77.Init(x);

+    this.data := y;

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

+    this.left := null;

+    this.right := gensym77;

+    // repr stuff

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

+  }

+

+

+  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;

@@ -184,54 +232,6 @@ class SetNode {
     this.Repr := ({this} + this.left.Repr) + this.right.Repr;

   }

 

-

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

-    modifies this;

-    requires x != y;

-    ensures fresh(Repr - {this});

-    ensures Valid();

-    ensures elems == {x, y};

-  {

-    if (y > x) {

-      this.DoubleBase(y, x);

-    } else {

-      this.DoubleBase(x, y);

-    }

-  }

-

-

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

-    modifies this;

-    requires x > y;

-    ensures fresh(Repr - {this});

-    ensures Valid();

-    ensures elems == {x, y};

-  {

-    var gensym77 := new SetNode;

-    gensym77.Init(x);

-    this.data := y;

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

-    this.left := null;

-    this.right := gensym77;

-    // repr stuff

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

-  }

-

-

-  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};

-  }

-

 }