Fixed some issues with assignments in refinements, both soundness bugs in previous version and changes necessitated by recent parsing refactoring

2 files changed, 36 insertions, 5 deletions

diff --git a/Test/dafny0/RefinementModificationChecking.dfy b/Test/dafny0/RefinementModificationChecking.dfy
index 34e30a05..70d0b989 100644
--- a/Test/dafny0/RefinementModificationChecking.dfy
+++ b/Test/dafny0/RefinementModificationChecking.dfy
@@ -10,7 +10,7 @@ abstract module R1 {
   }

 }

 

-abstract module R2 refines R1 {

+module R2 refines R1 {

   var g: nat;

   method m ...

   {

@@ -18,8 +18,36 @@ abstract module R2 refines R1 {
     var x := 3;

     t := {1}; // error: previous local

     r := 3; // error: out parameter

-    f := 4; // fine: all fields, will cause re-verification

+    f := 4; // error: previously defined field

     x := 6; // fine: new local

     g := 34;// fine: new field

   }

 }

+

+abstract module M0 {

+  class C {

+    method Init()

+      modifies this;

+    { }

+    method InitWithSideEffects(c: C)

+      modifies c;

+    { }

+    method mmm(arr: array<int>) {

+      var a: C :| true;

+      var b: C :| true;

+    }

+  }

+}

+

+module M1 refines M0 {

+  class C {

+    method mmm... {

+      var a := new C;  // fine

+      var b := new C.Init();  // fine

+      var c := new C.InitWithSideEffects(b);  // error: modifies previous state

+      if arr != null && 12 < arr.Length {

+        arr[12] := 26;  // error: modifies previously defined state

+      }

+    }

+  }

+}

diff --git a/Test/dafny0/RefinementModificationChecking.dfy.expect b/Test/dafny0/RefinementModificationChecking.dfy.expect
index 060ee3e4..675d244e 100644
--- a/Test/dafny0/RefinementModificationChecking.dfy.expect
+++ b/Test/dafny0/RefinementModificationChecking.dfy.expect
@@ -1,3 +1,6 @@
-RefinementModificationChecking.dfy(19,4): Error: cannot assign to variable defined previously

-RefinementModificationChecking.dfy(20,4): Error: cannot assign to variable defined previously

-2 resolution/type errors detected in RefinementModificationChecking.dfy

+RefinementModificationChecking.dfy(19,4): Error: refinement method cannot assign to variable defined in parent module ('t')

+RefinementModificationChecking.dfy(20,4): Error: refinement method cannot assign to variable defined in parent module ('r')

+RefinementModificationChecking.dfy(21,4): Error: refinement method cannot assign to a field defined in parent module ('f')

+RefinementModificationChecking.dfy(47,15): Error: assignment RHS in refinement method is not allowed to affect previously defined state

+RefinementModificationChecking.dfy(49,11): Error: new assignments in a refinement method can only assign to state that the module defines (which never includes array elements)

+5 resolution/type errors detected in RefinementModificationChecking.dfy