Dafny: better error reporting on resolution of refinements. Replace assertions with "if"s to handle errors gently and add cycle detection check.

1 files changed, 57 insertions, 0 deletions

diff --git a/Test/dafny0/RefinementErrors.dfy b/Test/dafny0/RefinementErrors.dfy
new file mode 100644
index 00000000..de8694b3
--- /dev/null
+++ b/Test/dafny0/RefinementErrors.dfy
@@ -0,0 +1,57 @@
+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)
+  {
+  }
+}
+
+class H refines E {
+  var x: int;
+
+  method M() 
+  {
+  }
+}
+
+class J refines E {
+  var y: int;
+  replaces x by x == y;
+
+  refines M()
+  {
+    y := 1;
+  }
+}
+
+