Jennisys:

   - small fixes to the modular synthesis

2 files changed, 82 insertions, 140 deletions

diff --git a/Jennisys/examples/mod2/jennisys-synth_Number.dfy b/Jennisys/examples/mod2/jennisys-synth_Number.dfy
index 3f1e6b4b..454a8548 100644
--- a/Jennisys/examples/mod2/jennisys-synth_Number.dfy
+++ b/Jennisys/examples/mod2/jennisys-synth_Number.dfy
@@ -25,116 +25,84 @@ class Number {
   }

 

 

-  method Double(p: int)

+  method Abs(a: int)

     modifies this;

     ensures fresh(Repr - {this});

     ensures Valid();

-    ensures num == 2 * p;

+    ensures num in {a, -a};

+    ensures num >= 0;

   {

-    this.num := 2 * p;

-    // repr stuff

-    this.Repr := {this};

+    if (a >= 0) {

+      this.Init(a);

+    } else {

+      this.Init(-a);

+    }

   }

 

 

-  method Init(p: int)

+  method Double(p: int)

     modifies this;

     ensures fresh(Repr - {this});

     ensures Valid();

-    ensures num == p;

+    ensures num == 2 * p;

   {

-    this.num := p;

-    // repr stuff

-    this.Repr := {this};

+    this.Init(2 * p);

   }

 

 

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

+  method Init(p: int)

     modifies this;

     ensures fresh(Repr - {this});

     ensures Valid();

-    ensures num == a + b;

+    ensures num == p;

   {

-    this.num := a + b;

+    this.num := p;

     // repr stuff

     this.Repr := {this};

   }

 

 

-  method Abs(a: int)

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

     modifies this;

     ensures fresh(Repr - {this});

     ensures Valid();

-    ensures num in {a, -a};

-    ensures num >= 0;

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

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

   {

-    if (a >= 0) {

-      this.num := a;

-      // repr stuff

-      this.Repr := {this};

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

+      this.Init(a);

     } else {

-      this.num := -a;

-      // repr stuff

-      this.Repr := {this};

+      this.Init(b);

     }

   }

 

 

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

+  method Min22(a: int, b: 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);

+    ensures num in {a, b};

+    ensures num <= a;

+    ensures num <= b;

   {

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

-      this.num := a;

-      // repr stuff

-      this.Repr := {this};

+    if (a <= b) {

+      this.Init(a);

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

-        }

-      }

+      this.Init(b);

     }

   }

 

 

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

+  method Min3(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;

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

+    ensures num <= a;

+    ensures num <= b;

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

-      }

-    }

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

   }

 

 

@@ -143,89 +111,68 @@ class Number {
     ensures fresh(Repr - {this});

     ensures Valid();

     ensures num in {a, b, c};

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

+    ensures num <= a;

+    ensures num <= b;

+    ensures num <= c;

   {

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

-      this.num := a;

-      // repr stuff

-      this.Repr := {this};

+      this.Init(a);

     } else {

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

-        this.num := c;

-        // repr stuff

-        this.Repr := {this};

+        this.Init(c);

       } else {

-        this.num := b;

-        // repr stuff

-        this.Repr := {this};

+        this.Init(b);

       }

     }

   }

 

 

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

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

     modifies this;

     ensures fresh(Repr - {this});

     ensures Valid();

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

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

     ensures num <= a;

     ensures num <= b;

     ensures num <= c;

+    ensures num <= d;

   {

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

-      this.num := a;

-      // repr stuff

-      this.Repr := {this};

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

+      this.Init(a);

     } else {

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

-        this.num := c;

-        // repr stuff

-        this.Repr := {this};

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

+        this.Init(d);

       } else {

-        this.num := b;

-        // repr stuff

-        this.Repr := {this};

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

+          this.Init(c);

+        } else {

+          this.Init(b);

+        }

       }

     }

   }

 

 

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

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

     modifies this;

     ensures fresh(Repr - {this});

     ensures Valid();

-    ensures num in {a, b};

-    ensures num <= a;

-    ensures num <= b;

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

+    ensures num <= a + b;

+    ensures num <= b + c;

+    ensures num <= a + c;

   {

-    if (a <= b) {

-      this.num := a;

-      // repr stuff

-      this.Repr := {this};

-    } else {

-      this.num := b;

-      // repr stuff

-      this.Repr := {this};

-    }

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

   }

 

 

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

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

     modifies this;

     ensures fresh(Repr - {this});

     ensures Valid();

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

-    ensures a >= b ==> num == b;

+    ensures num == a + b;

   {

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

-      this.num := a;

-      // repr stuff

-      this.Repr := {this};

-    } else {

-      this.num := b;

-      // repr stuff

-      this.Repr := {this};

-    }

+    this.Init(a + b);

   }

 

 }

diff --git a/Jennisys/examples/mod2/jennisys-synth_Set.dfy b/Jennisys/examples/mod2/jennisys-synth_Set.dfy
index c9584a5f..8449b03c 100644
--- a/Jennisys/examples/mod2/jennisys-synth_Set.dfy
+++ b/Jennisys/examples/mod2/jennisys-synth_Set.dfy
@@ -78,12 +78,7 @@ class Set {
     ensures Valid();

     ensures elems == {p + q};

   {

-    var gensym69 := new SetNode;

-    gensym69.Init(p + q);

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

-    this.root := gensym69;

-    // repr stuff

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

+    this.Singleton(p + q);

   }

 

 }

@@ -169,6 +164,27 @@ class SetNode {
   }

 

 

+  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 gensym80 := new SetNode;

+    var gensym81 := new SetNode;

+    gensym80.Init(z);

+    gensym81.Init(x);

+    this.data := y;

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

+    this.left := gensym81;

+    this.right := gensym80;

+    // repr stuff

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

+  }

+

+

   method Double(x: int, y: int)

     modifies this;

     requires x != y;

@@ -216,27 +232,6 @@ class SetNode {
     this.Repr := {this};

   }

 

-

-  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 gensym80 := new SetNode;

-    var gensym81 := new SetNode;

-    gensym80.Init(z);

-    gensym81.Init(x);

-    this.data := y;

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

-    this.left := gensym81;

-    this.right := gensym80;

-    // repr stuff

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

-  }

-

 }