Dafny: added support for simple superposition refinements

1 files changed, 13 insertions, 52 deletions

diff --git a/Test/dafny0/RefinementErrors.dfy b/Test/dafny0/RefinementErrors.dfy
index de8694b3..b10c035e 100644
--- a/Test/dafny0/RefinementErrors.dfy
+++ b/Test/dafny0/RefinementErrors.dfy
@@ -1,57 +1,18 @@
-class A refines C {
-}
-
-class B refines A {
-}
-
-class C refines B {
-}
-
-
-class D {
-  refines M()
-  {
-  }
-}
-
-class E {
-  var x: int;
-  
-  method M() 
-  {
-    x := 0;
-  }
-}
-
-class F {  
-  replaces M by x == y;
-}
-
-class G refines E {
-  var y: int;
-  replaces x by x == y;
-  
-  refines M() returns (i: int)
-  {
+module A {
+  class C {
+    method M(y: int) returns (x: int)
+    {
+      x := 6;
+    }
   }
 }
 
-class H refines E {
-  var x: int;
-
-  method M() 
-  {
+module B refines A {
+  class C {
+    var k: int;
+    method M(y: int) returns (x: int)
+      requires 0 <= y;  // error: cannot add a precondition
+      modifies this;  // error: cannot add a modifies clause
+      ensures 0 <= x;  // fine
   }
 }
-
-class J refines E {
-  var y: int;
-  replaces x by x == y;
-
-  refines M()
-  {
-    y := 1;
-  }
-}
-
-