diff options
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
}
}
}
|