diff options
author | Jason Koenig <unknown> | 2012-07-11 18:02:13 -0700 |
---|---|---|
committer | Jason Koenig <unknown> | 2012-07-11 18:02:13 -0700 |
commit | 5f2be2ca06c97c16bb9861255e949ffaf757ef69 (patch) | |
tree | 49537ee7cd09239ea48b3bdc8b059154ba81609d /Test/dafny2/StoreAndRetrieve.dfy | |
parent | 12497c67126499bc8c6a061d5840c711202ded28 (diff) |
Dafny: restored soundness for refinement by disallowing certain updates and method calls
Diffstat (limited to 'Test/dafny2/StoreAndRetrieve.dfy')
-rw-r--r-- | Test/dafny2/StoreAndRetrieve.dfy | 5 |
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
}
}
}
|