Change behavior of 'decreases *', which can be applied to loops and methods. Now, loops that may possibly

do an infinite number of iterations (that is, loops marked with 'decreases *') and calls to methods
marked with 'decreases *' are allowed only in methods that themselves are marked with 'decreases *'.  As
before, ghost loops and ghost methods are not allowed to be marked with 'decreases *'.

Previously, 'decreases *' was allowed on a method only if the method was tail recursive;
this is no longer so.  Note, however, that if the method is not tail recursive and engages
in infinite recursion, then it will eventually run out of stack space.

Previously, a 'decreases *' was not inherited in a refining module; this is no longer so.
That is, 'decreases *' is now inherited.  To refine a possibly non-terminating method
or loop, the refining version simply provides a decreases clause that does not mention '*'.
Note that if the refined method is not recursive, it still needs to have _some_ decreases
clause in order not to inherit the 'decreases *' from the refined method, but the expression
stated in the decreases clause can be arbitrary (for example, one can write 'decreases true'
or 'decreases 7' or 'decreases x' for some 'x' in scope).

Note, in the new design, a method needs to be declared with 'decreases *' if
it may recurse forever _or_ if it contains a possibly infinite loop.

Note that the absence of 'decreases *' on a loop does not mean the loop will
terminate, but it does mean that the loop will iterate a finite number of times
(the subtle distinction here is that a loop without a 'decreases *' is allowed
to contain a nested loop that has a 'decreases *' -- provided the enclosing
method is also declared with 'decreases *', as previously mentioned).

3 files changed, 6 insertions, 4 deletions

diff --git a/Test/dafny1/ListCopy.dfy b/Test/dafny1/ListCopy.dfy
index 4bffd51b..4bb2645c 100644
--- a/Test/dafny1/ListCopy.dfy
+++ b/Test/dafny1/ListCopy.dfy
@@ -12,6 +12,7 @@ class Node {
   }

 

   method Copy(root: Node) returns (result: Node)

+    decreases *;

   {

     var existingRegion: set<Node>;

     assume root == null || root in existingRegion;

diff --git a/Test/dafny1/ListReverse.dfy b/Test/dafny1/ListReverse.dfy
index 0837dd91..8d5a71e8 100644
--- a/Test/dafny1/ListReverse.dfy
+++ b/Test/dafny1/ListReverse.dfy
@@ -11,6 +11,7 @@ class Node {
     modifies r;

     ensures reverse == null || reverse in r;

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

+    decreases *;

   {

     var current := x;

     reverse := null;

diff --git a/Test/dafny1/SchorrWaite-stages.dfy b/Test/dafny1/SchorrWaite-stages.dfy
index a51a9fd0..854af021 100644
--- a/Test/dafny1/SchorrWaite-stages.dfy
+++ b/Test/dafny1/SchorrWaite-stages.dfy
@@ -54,6 +54,7 @@ abstract module M0 {
     ensures forall n :: n in S ==>

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

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

+    decreases *;  // leave termination checking for a later refinement

   {

     root.marked := true;

     var t, p := root, null;

@@ -159,8 +160,6 @@ abstract module M1 refines M0 {
       invariant forall n :: n in stackNodes || n == t ==>

                   n.marked &&

                   forall j :: 0 <= j < n.childrenVisited ==> n.children[j] == null || n.children[j].marked;

-

-      decreases *;  // keep postponing termination checking

     {

       if ... {  // pop

       } else if ... {  // next child

@@ -221,8 +220,6 @@ abstract module M2 refines M1 {
       invariant forall n :: n in S && n.marked ==> var pth := n.pathFromRoot;

                   !fresh(pth) && old(ReachableVia(root, pth, n, S));

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

-

-      decreases *;  // keep postponing termination checking

     {

       if ... {

         // pop

@@ -249,6 +246,9 @@ abstract module M2 refines M1 {
 module M3 refines M2 {

   // In this final superposition, we prove termination of the loop.

   method SchorrWaite...

+    decreases true;  // say that the method is now one that is proved to terminate (note, the value

+                     // 'true' is arbitrary; we just need to supply _some_ decreases clause so that

+                     // the 'decreases *' from above is not inherited)

   {

     // The loop variant is a lexicographic triple, consisting of (0) the set of unmarked

     // nodes, (1) the (length of the) stackNodes sequence, and (2) the number children of