From 5f2be2ca06c97c16bb9861255e949ffaf757ef69 Mon Sep 17 00:00:00 2001
From: Jason Koenig <unknown>
Date: Wed, 11 Jul 2012 18:02:13 -0700
Subject: Dafny: restored soundness for refinement by disallowing certain
 updates and method calls

---
 Test/dafny2/StoreAndRetrieve.dfy | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'Test/dafny2')

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
     }
   }
 }
-- 
cgit v1.2.3