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