1 files changed, 0 insertions, 137 deletions
diff --git a/Test/dafny0/NatTypes.dfy b/Test/dafny0/NatTypes.dfy
deleted file mode 100644
index 0513591c..00000000
--- a/Test/dafny0/NatTypes.dfy
+++ /dev/null
@@ -1,137 +0,0 @@
-method M(n: nat) {
-  assert 0 <= n;
-}
-
-method Main() {
-  M(25);
-  M(-25);  // error: cannot pass -25 as a nat
-}
-
-var f: nat;
-
-method CheckField(x: nat, y: int)
-  requires 0 <= y;
-  modifies this;
-{
-  var y: nat := y;
-
-  assert 0 <= f;
-  while (0 < y)
-  {
-    f := f + 1;
-    if (15 < f) {
-      f := f - 12;
-    }
-    y := y - 1;
-  }
-  assert 0 <= f;
-
-  f := x;  // no problem
-  f := x + 3;  // no problem here either
-  f := x - 3;  // error: cannot prove RHS is a nat
-}
-
-method Generic<T>(i: int, t0: T, t1: T) returns (r: T) {
-  if (0 < i) {
-    var n: nat := 5;
-    var j := Generic(i-1, n, -4);
-    assert 0 <= j;  // error: the result is an int, not a nat
-    var q := FenEric(n, -4);
-    assert 0 <= q;  // error: the result is an int, not a nat
-  }
-  r := t1;
-}
-
-function method FenEric<T>(t0: T, t1: T): T
-{
-  t1
-}
-
-datatype Pair<T> = Pr(T, T);
-
-method K(n: nat, i: int) {
-  match (Pair.Pr(n, i)) {
-    case Pr(k, l) =>
-      assert k == n;  // fine: although the type of k is int, we know it's equal to n
-      assert 0 <= k;
-      assert 0 <= l;  // error: l is an int
-  }
-}
-
-datatype List<T> = Nil | Cons(nat, T, List<T>);
-
-method MatchIt(list: List<object>) returns (k: nat)
-{
-  match (list) {
-    case Nil =>
-    case Cons(n, extra, tail) =>
-      var w := MatchIt(tail);
-      assert 0 <= w;
-      assert 0 <= n;  // fine
-      assert 0 <= n - 10;  // error: possible assertion failure
-  }
-
-  var m := Sum(list);
-  assert 0 <= m;
-  k := m;
-}
-
-class GenEric<T> {
-  var f: T;
-}
-
-function method GE<T>(d: GenEric<T>): bool { true }
-
-method TestGenEric() {
-  var ge;
-  if (ge != null) {
-    var b := GE(ge);
-    var n: nat := ge.f;  // error: the generic instantiation uses int, not nat
-  }
-}
-
-function method Sum(list: List<object>): nat
-{
-  match list
-  case Nil => 0
-  case Cons(x, y, tail) => x + Sum(tail)
-}
-
-function BadSum(list: List<object>): nat
-{
-  match list
-  case Nil => 0
-  case Cons(x, y, tail) => x + BadSum(tail) - 30  // error: may not be a nat
-}
-
-function Abs(x: int): nat
-{
-  if 0 <= x then x else -x
-}
-
-// ----- Here are tests that the type of the result value of a function is known by the
-// ----- time the well-formedness of the function's specification is checked.
-
-function TakesANat(n: nat): bool
-{
-  n < 29
-}
-
-function Naturally(): nat
-  ensures TakesANat(Naturally());  // the wellformedness of this check requires 
-{
-  17
-}
-
-function Integrally_Bad(): int
-  ensures TakesANat(Integrally_Bad());  // error: well-formedness check fails
-{
-  17
-}
-
-function Integrally_Good(): int
-  ensures 0 <= Integrally_Good();
-  ensures TakesANat(Integrally_Good());  // here, the needed information follows from the preceding ensures clause
-{
-  17
-}