* Added decreases clauses to functions

* If no decreases clause is given, the decreases clause defaults to the set of objects denoted by the reads clause, which was the previous Dafny behavior

* Made Dafny check loops for termination by default.  Previously, this was done only if the loop had a decreases clause.  To indicate that a loop is to be checked only for partial correctness, Dafny now allows "decreases *".

* Allow "reads *" to say that the function may read anything at all (sound, but not very useful)

* Adjusted frame axioms of functions to speak of allocated objects more liberally; and also added antecedents about the heaps being well-formed and the parameters being allocated

* Added some previously omitted well-definedness checks.

* Fixed some bugs in the resolver that caused some type errors not to be reported

* Added some messages to go with some (previously rather opaquely reported) errors

* Fixed some test cases that previously had ordered conjuncts incorrectly to prove termination and reads checks (such checks were previously omitted)

* Beefed up Test/dafny0/SchorrWaite.dfy to use datatypes to specify that no garbage gets marked.  The full-functional total-correctness verification of this Schorr-Waite method now takes about 3.2 seconds.

3 files changed, 6 insertions, 6 deletions

diff --git a/Test/VSI-Benchmarks/Answer b/Test/VSI-Benchmarks/Answer
index a9fd2367..954ca3b0 100644
--- a/Test/VSI-Benchmarks/Answer
+++ b/Test/VSI-Benchmarks/Answer
@@ -9,7 +9,7 @@ Dafny program verifier finished with 3 verified, 0 errors
 

 -------------------- b3.dfy --------------------

 

-Dafny program verifier finished with 4 verified, 0 errors

+Dafny program verifier finished with 5 verified, 0 errors

 

 -------------------- b4.dfy --------------------

 

@@ -29,4 +29,4 @@ Dafny program verifier finished with 11 verified, 0 errors
 

 -------------------- b8.dfy --------------------

 

-Dafny program verifier finished with 21 verified, 0 errors

+Dafny program verifier finished with 22 verified, 0 errors

diff --git a/Test/VSI-Benchmarks/b5.dfy b/Test/VSI-Benchmarks/b5.dfy
index 8026e60f..34ff5f57 100644
--- a/Test/VSI-Benchmarks/b5.dfy
+++ b/Test/VSI-Benchmarks/b5.dfy
@@ -17,8 +17,8 @@ class Queue<T> {
     tail.next == null &&

     (forall n ::

       n in spine ==>

-        n != null && n.Valid() &&

-        n.footprint <= footprint &&

+        n != null && n.footprint <= footprint && this !in n.footprint &&

+        n.Valid() &&

         (n.next == null ==> n == tail)) &&

     (forall n ::

       n in spine ==>

diff --git a/Test/VSI-Benchmarks/b8.dfy b/Test/VSI-Benchmarks/b8.dfy
index bc26ee85..a0cb6e74 100644
--- a/Test/VSI-Benchmarks/b8.dfy
+++ b/Test/VSI-Benchmarks/b8.dfy
@@ -59,7 +59,7 @@ class Glossary {
       invariant (forall d :: d in glossary.values ==> null !in d);

       invariant q !in rs.footprint;

       invariant q.contents == glossary.keys;

-      // we leave out the decreases clause - unbounded stream

+      decreases *;  // we leave out the decreases clause - unbounded stream

     {

       call term,definition := readDefinition(rs);

       if (term == null) {

@@ -135,7 +135,7 @@ class Glossary {
       while (true)

         invariant rs.Valid() && fresh(rs.footprint - old(rs.footprint));

         invariant null !in definition;

-        // we leave out the decreases clause - unbounded stream

+        decreases *;  // we leave out the decreases clause - unbounded stream

       {

         call w := rs.GetWord();

         if (w == null)