diff options
Diffstat (limited to 'Test/VSI-Benchmarks')
-rw-r--r-- | Test/VSI-Benchmarks/Answer | 16 | ||||
-rw-r--r-- | Test/VSI-Benchmarks/b2.dfy | 1 | ||||
-rw-r--r-- | Test/VSI-Benchmarks/b4.dfy | 5 | ||||
-rw-r--r-- | Test/VSI-Benchmarks/b5.dfy | 1 | ||||
-rw-r--r-- | Test/VSI-Benchmarks/b8.dfy | 6 |
5 files changed, 17 insertions, 12 deletions
diff --git a/Test/VSI-Benchmarks/Answer b/Test/VSI-Benchmarks/Answer index 954ca3b0..a0ae9d01 100644 --- a/Test/VSI-Benchmarks/Answer +++ b/Test/VSI-Benchmarks/Answer @@ -1,32 +1,32 @@ -------------------- b1.dfy --------------------
-Dafny program verifier finished with 2 verified, 0 errors
+Dafny program verifier finished with 4 verified, 0 errors
-------------------- b2.dfy --------------------
-Dafny program verifier finished with 3 verified, 0 errors
+Dafny program verifier finished with 6 verified, 0 errors
-------------------- b3.dfy --------------------
-Dafny program verifier finished with 5 verified, 0 errors
+Dafny program verifier finished with 10 verified, 0 errors
-------------------- b4.dfy --------------------
-Dafny program verifier finished with 6 verified, 0 errors
+Dafny program verifier finished with 11 verified, 0 errors
-------------------- b5.dfy --------------------
-Dafny program verifier finished with 12 verified, 0 errors
+Dafny program verifier finished with 22 verified, 0 errors
-------------------- b6.dfy --------------------
-Dafny program verifier finished with 12 verified, 0 errors
+Dafny program verifier finished with 21 verified, 0 errors
-------------------- b7.dfy --------------------
-Dafny program verifier finished with 11 verified, 0 errors
+Dafny program verifier finished with 23 verified, 0 errors
-------------------- b8.dfy --------------------
-Dafny program verifier finished with 22 verified, 0 errors
+Dafny program verifier finished with 42 verified, 0 errors
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..]);
diff --git a/Test/VSI-Benchmarks/b4.dfy b/Test/VSI-Benchmarks/b4.dfy index 3fa80b4c..ab1285f6 100644 --- a/Test/VSI-Benchmarks/b4.dfy +++ b/Test/VSI-Benchmarks/b4.dfy @@ -43,7 +43,8 @@ class Map<Key,Value> { requires Valid();
modifies this;
ensures Valid();
- ensures (forall i :: 0 <= i && i < |keys| && old(keys)[i] == key ==>
+ ensures (forall i :: 0 <= i && i < |old(keys)| && old(keys)[i] == key ==>
+ |keys| == |old(keys)| &&
keys[i] == key && values[i] == val &&
(forall j :: 0 <= j && j < |values| && i != j ==> keys[j] == old(keys)[j] && values[j] == old(values)[j]));
ensures key !in old(keys) ==> keys == old(keys) + [key] && values == old(values) + [val];
@@ -69,7 +70,7 @@ class Map<Key,Value> { // other values don't change:
ensures key !in old(keys) ==> keys == old(keys) && values == old(values);
ensures key in old(keys) ==>
- key !in keys &&
+ |keys| == |old(keys)| - 1 && key !in keys &&
(exists h ::
0 <= h && h <= |keys| &&
keys[..h] == old(keys)[..h] &&
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]);
{
diff --git a/Test/VSI-Benchmarks/b8.dfy b/Test/VSI-Benchmarks/b8.dfy index a0cb6e74..fec36c29 100644 --- a/Test/VSI-Benchmarks/b8.dfy +++ b/Test/VSI-Benchmarks/b8.dfy @@ -34,6 +34,7 @@ class Glossary { ensures r != null && fresh(r);
ensures |r.contents| == |old(q.contents)|;
ensures (forall i, j :: 0 <= i && i < j && j < |r.contents| ==>
+ r.Get(i) != null &&
r.Get(i).AtMost(r.Get(j)));
//perm is a permutation
ensures |perm| == |r.contents|; // ==|pperm|
@@ -289,7 +290,8 @@ class Map<Key,Value> { requires Valid();
modifies this;
ensures Valid();
- ensures (forall i :: 0 <= i && i < |keys| && old(keys)[i] == key ==>
+ ensures (forall i :: 0 <= i && i < |old(keys)| && old(keys)[i] == key ==>
+ |keys| == |old(keys)| &&
keys[i] == key && values[i] == val &&
(forall j :: 0 <= j && j < |values| && i != j ==> keys[j] == old(keys)[j] && values[j] == old(values)[j]));
ensures key !in old(keys) ==> keys == old(keys) + [key] && values == old(values) + [val];
@@ -315,7 +317,7 @@ class Map<Key,Value> { // other values don't change:
ensures key !in old(keys) ==> keys == old(keys) && values == old(values);
ensures key in old(keys) ==>
- key !in keys &&
+ |keys| == |old(keys)| - 1 && key !in keys &&
(exists h ::
0 <= h && h <= |keys| &&
keys[..h] == old(keys)[..h] &&
|