diff options
| author |  rustanleino <unknown> | 2010-03-12 09:46:44 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2010-03-12 09:46:44 +0000 |
| commit | aba99a56453354ee10f8c6d0b1b7ed3fbfe0d1e5 (patch) | |
| tree | cd3ec7755212a2ce28e6bc913f2683e4034b9639 /Test/VSI-Benchmarks/b2.dfy | |
| parent | 14e28e64aaae0c5620c2d2f2a3d13350b472b1e9 (diff) | |
Added wellformedness checks to method specifications
Diffstat (limited to 'Test/VSI-Benchmarks/b2.dfy')
| -rw-r--r-- | Test/VSI-Benchmarks/b2.dfy | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/Test/VSI-Benchmarks/b2.dfy b/Test/VSI-Benchmarks/b2.dfy index 6c0cfe81..457bc894 100644 --- a/Test/VSI-Benchmarks/b2.dfy +++ b/Test/VSI-Benchmarks/b2.dfy @@ -54,6 +54,7 @@ class Array { method Set(i: int, x: int);
requires 0 <= i && i < |contents|;
modifies this;
+ ensures |contents| == |old(contents)|;
ensures contents[..i] == old(contents[..i]);
ensures contents[i] == x;
ensures contents[i+1..] == old(contents[i+1..]);
|