diff options
author | 2010-03-12 09:46:44 +0000 | |
---|---|---|
committer | 2010-03-12 09:46:44 +0000 | |
commit | 0e6f265ca9a826dddd65b05ec21b97fcd549dccd (patch) | |
tree | 47aa45f17a019261a9c3eec99b109d0cf3cefd6e /Test/VSI-Benchmarks/b2.dfy | |
parent | e0a48b3b117393f7926c5723eb789db4fdea3267 (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..]);
|