Added wellformedness checks to method specifications

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] &&