diff options
author | rustanleino <unknown> | 2009-11-05 02:28:36 +0000 |
---|---|---|
committer | rustanleino <unknown> | 2009-11-05 02:28:36 +0000 |
commit | 3e050d0273c88db1b00c2d157ac1b970f2a5b4d7 (patch) | |
tree | 31bf1add9f2aba6a970d6eb21f3f83b987769e79 /Test/VSI-Benchmarks/b4.dfy | |
parent | ddede5ad5f9236d8ee4e1e75ba3ecfd7077d9296 (diff) |
The Dafny call statement now automatically declares left-hand sides as local variables, if they were not already local variables.
Diffstat (limited to 'Test/VSI-Benchmarks/b4.dfy')
-rw-r--r-- | Test/VSI-Benchmarks/b4.dfy | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/Test/VSI-Benchmarks/b4.dfy b/Test/VSI-Benchmarks/b4.dfy index ac58b7d1..5a9d46c8 100644 --- a/Test/VSI-Benchmarks/b4.dfy +++ b/Test/VSI-Benchmarks/b4.dfy @@ -30,7 +30,6 @@ class Map<Key,Value> { ensures present ==> (exists i :: 0 <= i && i < |keys| &&
keys[i] == key && values[i] == val);
{
- var j;
call j := FindIndex(key);
if (j == -1) {
present := false;
@@ -55,7 +54,6 @@ class Map<Key,Value> { ensures (forall i :: 0 <= i && i < |keys| && keys[i] != key ==>
values[i] == old(values)[i]);
{
- var j;
call j := FindIndex(key);
if (j == -1) {
keys := keys + [key];
@@ -88,7 +86,6 @@ class Map<Key,Value> { keys[h..] == old(keys)[h+1..] &&
values[h..] == old(values)[h+1..]);
{
- var j;
call j := FindIndex(key);
if (0 <= j) {
keys := keys[..j] + keys[j+1..];
|