Dafny: fixed bug in which old locals were not properly forbidden from being modified during refinement

1 files changed, 22 insertions, 0 deletions

diff --git a/Test/dafny0/RefinementModificationChecking.dfy b/Test/dafny0/RefinementModificationChecking.dfy
new file mode 100644
index 00000000..887c3595
--- /dev/null
+++ b/Test/dafny0/RefinementModificationChecking.dfy
@@ -0,0 +1,22 @@
+

+ghost module R1 {

+  var f: int;

+  method m(y: set<int>) returns (r: int)

+  {

+    var t := y;

+  }

+}

+

+ghost module R2 refines R1 {

+  var g: nat;

+  method m ...

+  {

+    ...;

+    var x := 3;

+    t := {1}; // bad: previous local

+    r := 3; // bad: out parameter

+    f := 4; // bad: previous field

+    x := 6; // fine: new local

+    g := 34;// fine: new field

+  }

+}