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

1 files changed, 4 insertions, 2 deletions

diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect
index ac44375d..a83051e7 100644
--- a/Test/dafny0/ResolutionErrors.dfy.expect
+++ b/Test/dafny0/ResolutionErrors.dfy.expect
@@ -134,7 +134,7 @@ ResolutionErrors.dfy(258,4): Error: label shadows an enclosing label
 ResolutionErrors.dfy(263,2): Error: duplicate label

 ResolutionErrors.dfy(289,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called

 ResolutionErrors.dfy(290,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called

-ResolutionErrors.dfy(292,4): Error: a constructor is only allowed to be called when an object is being allocated

+ResolutionErrors.dfy(292,4): Error: a constructor is allowed to be called only when an object is being allocated

 ResolutionErrors.dfy(306,16): Error: arguments must have the same type (got int and DTD_List)

 ResolutionErrors.dfy(307,16): Error: arguments must have the same type (got DTD_List and int)

 ResolutionErrors.dfy(308,25): Error: arguments must have the same type (got bool and int)

@@ -175,4 +175,6 @@ ResolutionErrors.dfy(960,7): Error: type conversion to real is allowed only from
 ResolutionErrors.dfy(961,7): Error: type conversion to int is allowed only from real (got int)

 ResolutionErrors.dfy(962,7): Error: type conversion to int is allowed only from real (got nat)

 ResolutionErrors.dfy(1101,8): Error: new cannot be applied to a trait

-177 resolution/type errors detected in ResolutionErrors.dfy

+ResolutionErrors.dfy(1122,2): Error: a call to a possibly non-terminating method is allowed only if the calling method is also declared (with 'decreases *') to be possibly non-terminating

+ResolutionErrors.dfy(1137,14): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating

+179 resolution/type errors detected in ResolutionErrors.dfy