1 files changed, 130 insertions, 0 deletions
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};
+  }
+
+}
+
+