1 files changed, 0 insertions, 193 deletions
diff --git a/Test/dafny0/Refinement.dfy b/Test/dafny0/Refinement.dfy
deleted file mode 100644
index e5c06a5e..00000000
--- a/Test/dafny0/Refinement.dfy
+++ /dev/null
@@ -1,193 +0,0 @@
-module A {
-  class X { }
-  class T {
-    method M(x: int) returns (y: int)
-      requires 0 <= x;
-      ensures 0 <= y;
-    {
-      y := 2 * x;
-    }
-    method Q() returns (q: int, r: int, s: int)
-      ensures 0 <= q && 0 <= r && 0 <= s;
-    {  // error: failure to establish postcondition about q
-      r, s := 100, 200;
-    }
-  }
-}
-
-module B refines A {
-  class C { }
-  datatype Dt = Ax | Bx;
-  class T {
-    method P() returns (p: int)
-    {
-      p := 18;
-    }
-    method M(x: int) returns (y: int)
-      ensures y % 2 == 0;  // add a postcondition
-    method Q ...
-      ensures 12 <= r;
-      ensures 1200 <= s;  // error: postcondition is not established by
-                          // inherited method body
-  }
-}
-
-// ------------------------------------------------
-
-module A_AnonymousClass {
-  var x: int;
-  method Increment(d: int)
-    modifies this;
-  {
-    x := x + d;
-  }
-}
-
-module B_AnonymousClass refines A_AnonymousClass {
-  method Increment...
-    ensures x <= old(x) + d;
-}
-
-module C_AnonymousClass refines B_AnonymousClass {
-  method Increment(d: int)
-    ensures old(x) + d <= x;
-  method Main()
-    modifies this;
-  {
-    x := 25;
-    Increment(30);
-    assert x == 55;
-    Increment(12);
-    assert x == 66;  // error: it's 67
-  }
-}
-
-// ------------------------------------------------
-
-module BodyFree {
-  function F(x: int): int
-    ensures 0 <= F(x);
-  method TestF() {
-    assert F(6) == F(7);  // error: no information about F so far
-  }
-  method M() returns (a: int, b: int)
-    ensures a == b;
-}
-
-module SomeBody refines BodyFree {
-  function F(x: int): int
-  { if x < 0 then 2 else 3 }
-  method TestFAgain() {
-    assert F(6) == F(7);
-  }
-  method M() returns (a: int, b: int)
-  {
-    a := b;  // good
-  }
-}
-
-module FullBodied refines BodyFree {
-  function F(x: int): int
-  { x } // error: does not meet the inherited postcondition
-  method M() returns (a: int, b: int)
-  {  // error: does not establish postcondition
-    a := b + 1;
-  }
-}
-
-// ------------------------------------------------
-
-module Abstract {
-  class MyNumber {
-    ghost var N: int;
-    ghost var Repr: set<object>;
-    predicate Valid
-      reads this, Repr;
-    {
-      this in Repr && null !in Repr
-    }
-    constructor Init()
-      modifies this;
-      ensures N == 0;
-      ensures Valid && fresh(Repr - {this});
-    {
-      N, Repr := 0, {this};
-    }
-    method Inc()
-      requires Valid;
-      modifies Repr;
-      ensures N == old(N) + 1;
-      ensures Valid && fresh(Repr - old(Repr));
-    {
-      N := N + 1;
-    }
-    method Get() returns (n: int)
-      requires Valid;
-      ensures n == N;
-    {
-      var k;  assume k == N;
-      n := k;
-    }
-  }
-}
-
-module Concrete refines Abstract {
-  class MyNumber {
-    var a: int;
-    var b: int;
-    predicate Valid
-    {
-      N == a - b
-    }
-    constructor Init()
-    {
-      a := b;
-    }
-    method Inc()
-    {
-      if (*) { a := a + 1; } else { b := b - 1; }
-    }
-    method Get() returns (n: int)
-    {
-      var k := a - b;
-      assert ...;
-    }
-  }
-}
-
-module Client {
-  import C = Concrete;
-  class TheClient {
-    method Main() {
-      var n := new C.MyNumber.Init();
-      n.Inc();
-      n.Inc();
-      var k := n.Get();
-      assert k == 2;
-    }
-  }
-}
-
-module IncorrectConcrete refines Abstract {
-  class MyNumber {
-    var a: int;
-    var b: int;
-    predicate Valid
-    {
-      N == 2*a - b
-    }
-    constructor Init()
-    {  // error: postcondition violation
-      a := b;
-    }
-    method Inc()
-    {  // error: postcondition violation
-      if (*) { a := a + 1; } else { b := b - 1; }
-    }
-    method Get() returns (n: int)
-    {
-      var k := a - b;
-      assert ...;  // error: assertion violation
-    }
-  }
-}