Dafny: restored soundness for refinement by disallowing certain updates and method calls

1 files changed, 4 insertions, 1 deletions

diff --git a/Test/dafny2/StoreAndRetrieve.dfy b/Test/dafny2/StoreAndRetrieve.dfy
index 9ea7a3ff..dce9795b 100644
--- a/Test/dafny2/StoreAndRetrieve.dfy
+++ b/Test/dafny2/StoreAndRetrieve.dfy
@@ -51,6 +51,9 @@ module B refines A {
         i := i + 1;

       }

       var k := arr[i];

+      ...;

+      var a :| Contents == set x | x in a;

+      arr := a;

     }

   }

 }

@@ -60,7 +63,7 @@ module C refines B {
     method Retrieve...

     {

       ...;

-      arr := [thing] + arr[..i] + arr[i+1..];  // LRU behavior

+      var a := [thing] + arr[..i] + arr[i+1..];  // LRU behavior

     }

   }

 }