diff options
Diffstat (limited to 'Test/VSI-Benchmarks/b4.dfy')
-rw-r--r-- | Test/VSI-Benchmarks/b4.dfy | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/Test/VSI-Benchmarks/b4.dfy b/Test/VSI-Benchmarks/b4.dfy index ebaeab84..9f7e272e 100644 --- a/Test/VSI-Benchmarks/b4.dfy +++ b/Test/VSI-Benchmarks/b4.dfy @@ -88,7 +88,7 @@ class Map<Key,Value> { }
}
- method Remove(key: Key)
+ method Remove(key: Key)// returns (ghost h: int)
requires Valid();
modifies Repr;
ensures Valid() && fresh(Repr - old(Repr));
@@ -111,6 +111,9 @@ class Map<Key,Value> { if (p != null) {
Keys := Keys[..n] + Keys[n+1..];
Values := Values[..n] + Values[n+1..];
+ assert Keys[n..] == old(Keys)[n+1..];
+ assert Values[n..] == old(Values)[n+1..];
+
nodes := nodes[..n] + nodes[n+1..];
if (prev == null) {
head := head.next;
|