diff options
Diffstat (limited to 'Test/VSI-Benchmarks/b5.dfy')
| -rw-r--r-- | Test/VSI-Benchmarks/b5.dfy | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/Test/VSI-Benchmarks/b5.dfy b/Test/VSI-Benchmarks/b5.dfy index 34ff5f57..2e274845 100644 --- a/Test/VSI-Benchmarks/b5.dfy +++ b/Test/VSI-Benchmarks/b5.dfy @@ -109,6 +109,7 @@ class Queue<T> { requires 0 < |contents|;
modifies footprint;
ensures Valid() && fresh(footprint - old(footprint));
+ ensures |contents| == |old(contents)|;
ensures (exists i :: 0 <= i && i <= |contents| &&
contents == old(contents)[i..] + old(contents)[..i]);
{
|