1 files changed, 0 insertions, 130 deletions
diff --git a/Jennisys/Jennisys/examples/oopsla12/IntSet_synth.dfy b/Jennisys/Jennisys/examples/oopsla12/IntSet_synth.dfy
deleted file mode 100644
index 55523e79..00000000
--- a/Jennisys/Jennisys/examples/oopsla12/IntSet_synth.dfy
+++ /dev/null
@@ -1,130 +0,0 @@
-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};
-  }
-
-}
-
-