* 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.

15 files changed, 112 insertions, 33 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)

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 62457ec4..043a4cfd 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -56,8 +56,18 @@ Dafny program verifier finished with 0 verified, 0 errors
 

 Boogie program verifier finished with 8 verified, 0 errors

 

+-------------------- TypeTests.dfy --------------------

+TypeTests.dfy(4,13): Error: incorrect type of function argument 0 (expected C, got D)

+TypeTests.dfy(4,13): Error: incorrect type of function argument 1 (expected D, got C)

+TypeTests.dfy(5,13): Error: incorrect type of function argument 0 (expected C, got int)

+TypeTests.dfy(5,13): Error: incorrect type of function argument 1 (expected D, got int)

+TypeTests.dfy(11,4): Error: incorrect type of method in-parameter 0 (expected int, got bool)

+TypeTests.dfy(12,4): Error: incorrect type of method out-parameter 0 (expected int, got C)

+TypeTests.dfy(12,4): Error: incorrect type of method out-parameter 1 (expected C, got int)

+7 resolution/type errors detected in synthetic program

+

 -------------------- SmallTests.dfy --------------------

-SmallTests.dfy(29,7): Error: RHS expression must be well defined

+SmallTests.dfy(30,7): Error: RHS expression must be well defined

 Execution trace:

     (0,0): anon0

 

@@ -85,47 +95,47 @@ Dafny program verifier finished with 5 verified, 0 errors
 

 -------------------- SchorrWaite.dfy --------------------

 

-Dafny program verifier finished with 4 verified, 0 errors

+Dafny program verifier finished with 6 verified, 0 errors

 

 -------------------- Termination.dfy --------------------

 

 Dafny program verifier finished with 6 verified, 0 errors

 

 -------------------- Use.dfy --------------------

-Use.dfy(12,5): Error BP5001: This assertion might not hold.

+Use.dfy(12,5): Error: assertion violation

 Execution trace:

     (0,0): anon0

-Use.dfy(25,5): Error BP5001: This assertion might not hold.

+Use.dfy(25,5): Error: assertion violation

 Execution trace:

     (0,0): anon0

-Use.dfy(50,5): Error BP5001: This assertion might not hold.

+Use.dfy(50,5): Error: assertion violation

 Execution trace:

     (0,0): anon0

 

 Dafny program verifier finished with 6 verified, 3 errors

 

 -------------------- DTypes.dfy --------------------

-DTypes.dfy(15,5): Error BP5001: This assertion might not hold.

+DTypes.dfy(15,5): Error: assertion violation

 Execution trace:

     (0,0): anon0

-DTypes.dfy(28,5): Error BP5001: This assertion might not hold.

+DTypes.dfy(28,5): Error: assertion violation

 Execution trace:

     (0,0): anon0

-DTypes.dfy(54,5): Error BP5001: This assertion might not hold.

+DTypes.dfy(54,5): Error: assertion violation

 Execution trace:

     (0,0): anon0

 

 Dafny program verifier finished with 5 verified, 3 errors

 

 -------------------- TypeParameters.dfy --------------------

-TypeParameters.dfy(41,5): Error BP5001: This assertion might not hold.

+TypeParameters.dfy(41,5): Error: assertion violation

 Execution trace:

     (0,0): anon0

-TypeParameters.dfy(63,5): Error BP5001: This assertion might not hold.

+TypeParameters.dfy(63,5): Error: assertion violation

 Execution trace:

     (0,0): anon0

 

-Dafny program verifier finished with 9 verified, 2 errors

+Dafny program verifier finished with 10 verified, 2 errors

 

 -------------------- Datatypes.dfy --------------------

 

diff --git a/Test/dafny0/BinaryTree.dfy b/Test/dafny0/BinaryTree.dfy
index 138a22df..54a98a56 100644
--- a/Test/dafny0/BinaryTree.dfy
+++ b/Test/dafny0/BinaryTree.dfy
@@ -10,9 +10,9 @@ class IntSet {
     this in footprint &&

     (root == null ==> contents == {}) &&

     (root != null ==>

-       root in footprint && root.Valid() &&

-       contents == root.contents &&

-       root.footprint <= footprint && this !in root.footprint)

+       root in footprint && root.footprint <= footprint && this !in root.footprint &&

+       root.Valid() &&

+       contents == root.contents)

   }

 

   method Init()

@@ -110,12 +110,14 @@ class Node {
     this in footprint &&

     null !in footprint &&

     (left != null ==>

-      left in footprint && left.Valid() &&

+      left in footprint &&

       left.footprint <= footprint && this !in left.footprint &&

+      left.Valid() &&

       (forall y :: y in left.contents ==> y < data)) &&

     (right != null ==>

-      right in footprint && right.Valid() &&

+      right in footprint &&

       right.footprint <= footprint && this !in right.footprint &&

+      right.Valid() &&

       (forall y :: y in right.contents ==> data < y)) &&

     (left == null && right == null ==>

       contents == {data}) &&

diff --git a/Test/dafny0/DTypes.dfy b/Test/dafny0/DTypes.dfy
index c468cff4..c6f0737c 100644
--- a/Test/dafny0/DTypes.dfy
+++ b/Test/dafny0/DTypes.dfy
@@ -58,7 +58,9 @@ class C {
   {

     var a := new CP<int,C>;

     var b := new CP<int,object>;

-    while (a != null) {

+    while (a != null)

+      decreases *;  // omit loop termination check (in fact, the loop does not terminate)

+    {

       var x: object := a;

       var y: object := b;

       assert x == y ==> x == null;

diff --git a/Test/dafny0/Datatypes.dfy b/Test/dafny0/Datatypes.dfy
index 61ae9cb6..8492f217 100644
--- a/Test/dafny0/Datatypes.dfy
+++ b/Test/dafny0/Datatypes.dfy
@@ -8,7 +8,8 @@ class Node {
   var next: Node;

 

   function Repr(list: List<int>): bool

-    reads this;

+    reads *;

+    decreases list;

   { match list

     case Nil =>

       next == null

@@ -38,7 +39,8 @@ class AnotherNode {
   var next: AnotherNode;

 

   function Repr(n: AnotherNode, list: List<int>): bool

-    reads n;

+    reads *;

+    decreases list;

   { match list

     case Nil =>

       n == null

diff --git a/Test/dafny0/ListContents.dfy b/Test/dafny0/ListContents.dfy
index 759c6afd..952c47d2 100644
--- a/Test/dafny0/ListContents.dfy
+++ b/Test/dafny0/ListContents.dfy
@@ -75,6 +75,7 @@ class Node<T> {
         (forall i :: 0 <= i && i < |current.list| ==> current.list[i] == old(list)[|reverse.list|+i]);

       invariant

         (forall i :: 0 <= i && i < |reverse.list| ==> old(list)[i] == reverse.list[|reverse.list|-1-i]);

+      decreases current, |current.list|;

     {

       var nx := current.next;

       assert nx != null ==> (forall i :: 0 <= i && i < |nx.list| ==> current.list[1+i] == nx.list[i]); // lemma

diff --git a/Test/dafny0/ListCopy.dfy b/Test/dafny0/ListCopy.dfy
index f3c64fe2..52f5cf76 100644
--- a/Test/dafny0/ListCopy.dfy
+++ b/Test/dafny0/ListCopy.dfy
@@ -31,6 +31,7 @@ class Node {
         invariant prev in newRegion;

         invariant fresh(newRegion);

         invariant newRegion !! existingRegion;

+        decreases *;  // omit loop termination check

       {

         var tmp := new Node;

         call tmp.Init();

diff --git a/Test/dafny0/ListReverse.dfy b/Test/dafny0/ListReverse.dfy
index 08b14751..ef029b88 100644
--- a/Test/dafny0/ListReverse.dfy
+++ b/Test/dafny0/ListReverse.dfy
@@ -16,6 +16,7 @@ class Node {
       invariant current == null || current in r;

       invariant reverse == null || reverse in r;

       invariant (forall y :: y in r ==> y.nxt == null || y.nxt in r);  // region closure

+      decreases *;  // omit loop termination check

     {

       var tmp := current.nxt;

       current.nxt := reverse;

diff --git a/Test/dafny0/Queue.dfy b/Test/dafny0/Queue.dfy
index 5c22ec92..da1ab2c5 100644
--- a/Test/dafny0/Queue.dfy
+++ b/Test/dafny0/Queue.dfy
@@ -17,12 +17,12 @@ class Queue<T> {
     head != null && head in spine &&

     tail != null && tail in spine &&

     tail.next == null &&

-    (forall n ::  // { n in spine }

+    (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.next }

+    (forall n ::

       n in spine ==>

         n.next != null ==> n.next in spine) &&

     contents == head.tailContents

diff --git a/Test/dafny0/SchorrWaite.dfy b/Test/dafny0/SchorrWaite.dfy
index 20db882a..527d379f 100644
--- a/Test/dafny0/SchorrWaite.dfy
+++ b/Test/dafny0/SchorrWaite.dfy
@@ -7,6 +7,7 @@ class Node {
   var marked: bool;

   var childrenVisited: int;

   var children: seq<Node>;

+  var pathFromRoot: Path;  // used only as ghost variable

 }

 

 class Main {

@@ -61,11 +62,13 @@ class Main {
         invariant (forall n :: n in S ==>

                 n.childrenVisited == old(n.childrenVisited) &&

                 n.children == old(n.children));

+        decreases |root.children| - i;

       {

         var c := root.children[i];

         if (c != null) {

           call RecursiveMarkWorker(c, S, stackNodes + {root});

         }

+        i := i + 1;

       }

     }

   }

@@ -140,24 +143,48 @@ class Main {
 

   // ---------------------------------------------------------------------------------

 

+  function Reachable(from: Node, to: Node, S: set<Node>): bool

+    requires null !in S;

+    reads S;

+    decreases 1;

+  {

+    (exists via: Path :: ReachableVia(from, via, to, S))

+  }

+

+  function ReachableVia(from: Node, via: Path, to: Node, S: set<Node>): bool

+    requires null !in S;

+    reads S;

+    decreases 0, via;

+  {

+    match via

+    case Empty => from == to

+    case Extend(prefix, n) => n in S && to in n.children && ReachableVia(from, prefix, n, S)

+  }

+

   method SchorrWaite(root: Node, S: set<Node>)

     requires root in S;

     // S is closed under 'children':

     requires (forall n :: n in S ==> n != null &&

                 (forall ch :: ch in n.children ==> ch == null || ch in S));

+    // the graph starts off with nothing marked and nothing being indicated as currently being visited

     requires (forall n :: n in S ==> ! n.marked && n.childrenVisited == 0);

     modifies S;

-    ensures root.marked;

     // nodes reachable from 'root' are marked:

+    ensures root.marked;

     ensures (forall n :: n in S && n.marked ==>

                 (forall ch :: ch in n.children && ch != null ==> ch in S && ch.marked));

+    // every marked node was reachable from 'root' in the pre-state

+    ensures (forall n :: n in S && n.marked ==> old(Reachable(root, n, S)));

+    // the graph has not changed

     ensures (forall n :: n in S ==>

                 n.childrenVisited == old(n.childrenVisited) &&

                 n.children == old(n.children));

   {

     var t := root;

     var p: Node := null;  // parent of t in original graph

+    var path := #Path.Empty;

     t.marked := true;

+    t.pathFromRoot := path;

     var stackNodes := [];  // used as ghost variable

     var unmarkedNodes := S - {t};  // used as ghost variable

     while (true)

@@ -183,6 +210,11 @@ class Main {
                   |n.children| == old(|n.children|) &&

                   (forall j :: 0 <= j && j < |n.children| ==>

                     j == n.childrenVisited || n.children[j] == old(n.children[j])));

+      // every marked node is reachable

+      invariant old(ReachableVia(root, path, t, S));

+      invariant (forall n, pth :: n in S && n.marked && pth == n.pathFromRoot ==>

+                  old(ReachableVia(root, pth, n, S)));

+      invariant (forall n :: n in S && n.marked ==> old(Reachable(root, n, S)));

       // the current values of m.children[m.childrenVisited] for m's on the stack:

       invariant 0 < |stackNodes| ==> stackNodes[0].children[stackNodes[0].childrenVisited] == null;

       invariant (forall k :: 0 < k && k < |stackNodes| ==>

@@ -208,10 +240,12 @@ class Main {
         p := oldP;

         stackNodes := stackNodes[..|stackNodes| - 1];

         t.childrenVisited := t.childrenVisited + 1;

+        path := t.pathFromRoot;

 

       } else if (t.children[t.childrenVisited] == null || t.children[t.childrenVisited].marked) {

         // just advance to next child

         t.childrenVisited := t.childrenVisited + 1;

+

       } else {

         // push

 

@@ -220,10 +254,17 @@ class Main {
         t.children := t.children[..t.childrenVisited] + [p] + t.children[t.childrenVisited + 1..];

         p := t;

         stackNodes := stackNodes + [t];

+        path := #Path.Extend(path, t);

         t := newT;

         t.marked := true;

+        t.pathFromRoot := path;

         unmarkedNodes := unmarkedNodes - {t};

       }

     }

   }

 }

+

+datatype Path {

+  Empty;

+  Extend(Path, Node);

+}

diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy
index 01c9f1ea..17f0168a 100644
--- a/Test/dafny0/SmallTests.dfy
+++ b/Test/dafny0/SmallTests.dfy
@@ -2,9 +2,10 @@ class Node {
   var next: Node;

 

   function IsList(r: set<Node>): bool

-    reads this, r; 

+    reads r; 

   {

-    next != null  ==>  next.IsList(r - {this})

+    this in r &&

+    (next != null  ==>  next.IsList(r - {this}))

   }

 

   method Test(n: Node, nodes: set<Node>) 

diff --git a/Test/dafny0/TypeTests.dfy b/Test/dafny0/TypeTests.dfy
new file mode 100644
index 00000000..4cb02858
--- /dev/null
+++ b/Test/dafny0/TypeTests.dfy
@@ -0,0 +1,18 @@
+class C {

+  function F(c: C, d: D): bool { true }

+  method M(x: int) returns (y: int, c: C)

+    requires F(#D.A, this);  // 2 errors

+    requires F(4, 5);  // 2 errors

+    requires F(this, #D.A);  // good

+  { }

+

+  method Caller()

+  {

+    call m,n := M(true);  // error on in-parameter

+    call n,m := M(m);  // 2 errors on out-parameters

+  }

+}

+

+datatype D {

+  A;

+}

diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index 4fa6832e..f1bcfde0 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -17,7 +17,7 @@ for %%f in (BQueue.bpl) do (
   %BPLEXE% %* %%f

 )

 

-for %%f in (SmallTests.dfy Queue.dfy ListCopy.dfy

+for %%f in (TypeTests.dfy SmallTests.dfy Queue.dfy ListCopy.dfy

             BinaryTree.dfy ListReverse.dfy ListContents.dfy

             SchorrWaite.dfy Termination.dfy Use.dfy DTypes.dfy

             TypeParameters.dfy Datatypes.dfy) do (