diff options
Diffstat (limited to 'Test')
| -rw-r--r-- | Test/VSI-Benchmarks/b3.dfy | 3 | ||||
| -rw-r--r-- | Test/dafny0/DirtyLoops.dfy | 12 | ||||
| -rw-r--r-- | Test/dafny0/DirtyLoops.dfy.expect | 2 |
3 files changed, 14 insertions, 3 deletions
diff --git a/Test/VSI-Benchmarks/b3.dfy b/Test/VSI-Benchmarks/b3.dfy index 91044397..5a2b6e13 100644 --- a/Test/VSI-Benchmarks/b3.dfy +++ b/Test/VSI-Benchmarks/b3.dfy @@ -86,8 +86,8 @@ class Benchmark3 { while (j < n)
invariant j <= n;
+ invariant 0 <= k < n && old(q.contents)[k] == m;
invariant q.contents == old(q.contents)[j..] + old(q.contents)[..j]; //i.e. rotated
- invariant 0 <= k < |old(q.contents)| && old(q.contents)[k] == m;
invariant forall i :: 0 <= i < j ==> m <= old(q.contents)[i]; //m is min so far
{
var x := q.Dequeue();
@@ -104,7 +104,6 @@ class Benchmark3 { var x := q.Dequeue();
q.Enqueue(x);
j := j+1;
- assert q.contents == old(q.contents)[j..] + old(q.contents)[..j];
}
m := q.Dequeue();
diff --git a/Test/dafny0/DirtyLoops.dfy b/Test/dafny0/DirtyLoops.dfy index d3164fa9..b283756b 100644 --- a/Test/dafny0/DirtyLoops.dfy +++ b/Test/dafny0/DirtyLoops.dfy @@ -19,3 +19,15 @@ method M2(x: int) invariant i <= x;
decreases i;
}
+
+var f: int;
+
+method M3(x: int)
+ requires f <= x;
+ modifies `f;
+{
+ while (0 < f)
+ invariant f <= x;
+ decreases f;
+ modifies `f;
+}
diff --git a/Test/dafny0/DirtyLoops.dfy.expect b/Test/dafny0/DirtyLoops.dfy.expect index 060f3287..99fb4165 100644 --- a/Test/dafny0/DirtyLoops.dfy.expect +++ b/Test/dafny0/DirtyLoops.dfy.expect @@ -1,4 +1,4 @@ -Dafny program verifier finished with 6 verified, 0 errors
+Dafny program verifier finished with 8 verified, 0 errors
Dafny program verifier finished with 0 verified, 0 errors
|