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

22 files changed, 193 insertions, 99 deletions

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index deef9285..711fadf0 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -639,7 +639,7 @@ MethodDecl<MemberModifiers mmod, bool allowConstructor, out Method/*!*/ m>
   | "constructor"                   (. if (allowConstructor) {

                                          isConstructor = true;

                                        } else {

-                                         SemErr(t, "constructors are only allowed in classes");

+                                         SemErr(t, "constructors are allowed only in classes");

                                        }

                                     .)

   )                                 (. keywordToken = t; .)

@@ -1407,13 +1407,13 @@ Invariant<out MaybeFreeExpression/*!*/ invariant>
 DecreasesList<.List<Expression/*!*/> decreases, bool allowWildcard.>

 = (. Expression/*!*/ e; .)

   PossiblyWildExpression<out e>          (. if (!allowWildcard && e is WildcardExpr) {

-                                              SemErr(e.tok, "'decreases *' is only allowed on loops and tail-recursive methods");

+                                              SemErr(e.tok, "'decreases *' is allowed only on loops and tail-recursive methods");

                                             } else {

                                               decreases.Add(e);

                                             }

                                          .)

   { "," PossiblyWildExpression<out e>    (. if (!allowWildcard && e is WildcardExpr) {

-                                              SemErr(e.tok, "'decreases *' is only allowed on loops and tail-recursive methods");

+                                              SemErr(e.tok, "'decreases *' is allowed only on loops and tail-recursive methods");

                                             } else {

                                               decreases.Add(e);

                                             }

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 08d05fab..f1e39604 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -1816,6 +1816,7 @@ namespace Microsoft.Dafny {
     ModuleDefinition EnclosingModule { get; }  // to be called only after signature-resolution is complete

     bool MustReverify { get; }

     string FullSanitizedName { get; }

+    bool AllowsNontermination { get; }

   }

   /// <summary>

   /// An ICallable is a Function, Method, or IteratorDecl.

@@ -1858,6 +1859,7 @@ namespace Microsoft.Dafny {
     ModuleDefinition ICodeContext.EnclosingModule { get { return Module; } }

     bool ICodeContext.MustReverify { get { Contract.Assume(false, "should not be called on NoContext"); throw new cce.UnreachableException(); } }

     public string FullSanitizedName { get { Contract.Assume(false, "should not be called on NoContext"); throw new cce.UnreachableException(); } }

+    public bool AllowsNontermination { get { Contract.Assume(false, "should not be called on NoContext"); throw new cce.UnreachableException(); } }

   }

 

   public class IteratorDecl : ClassDecl, IMethodCodeContext

@@ -1959,6 +1961,11 @@ namespace Microsoft.Dafny {
     }

     ModuleDefinition ICodeContext.EnclosingModule { get { return this.Module; } }

     bool ICodeContext.MustReverify { get { return false; } }

+    public bool AllowsNontermination {

+      get {

+        return Contract.Exists(Decreases.Expressions, e => e is WildcardExpr);

+      }

+    }

   }

 

   public abstract class MemberDecl : Declaration {

@@ -2451,6 +2458,12 @@ namespace Microsoft.Dafny {
       }

     }

 

+    public bool AllowsNontermination {

+      get {

+        return Contract.Exists(Decreases.Expressions, e => e is WildcardExpr);

+      }

+    }

+

     /// <summary>

     /// The "AllCalls" field is used for non-CoPredicate, non-PrefixPredicate functions only (so its value should not be relied upon for CoPredicate and PrefixPredicate functions).

     /// It records all function calls made by the Function, including calls made in the body as well as in the specification.

@@ -2683,6 +2696,11 @@ namespace Microsoft.Dafny {
       }

     }

     bool ICodeContext.MustReverify { get { return this.MustReverify; } }

+    public bool AllowsNontermination {

+      get {

+        return Contract.Exists(Decreases.Expressions, e => e is WildcardExpr);

+      }

+    }

   }

 

   public class Lemma : Method

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 9da363a2..740a7189 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -971,7 +971,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
 			if (allowConstructor) {

 			 isConstructor = true;

 			} else {

-			 SemErr(t, "constructors are only allowed in classes");

+			 SemErr(t, "constructors are allowed only in classes");

 			}

 			

 		} else SynErr(150);

@@ -1532,7 +1532,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Expression/*!*/ e; 

 		PossiblyWildExpression(out e);

 		if (!allowWildcard && e is WildcardExpr) {

-		 SemErr(e.tok, "'decreases *' is only allowed on loops and tail-recursive methods");

+		 SemErr(e.tok, "'decreases *' is allowed only on loops and tail-recursive methods");

 		} else {

 		 decreases.Add(e);

 		}

@@ -1541,7 +1541,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Get();

 			PossiblyWildExpression(out e);

 			if (!allowWildcard && e is WildcardExpr) {

-			 SemErr(e.tok, "'decreases *' is only allowed on loops and tail-recursive methods");

+			 SemErr(e.tok, "'decreases *' is allowed only on loops and tail-recursive methods");

 			} else {

 			 decreases.Add(e);

 			}

diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs
index a7989cba..afdd640b 100644
--- a/Source/Dafny/RefinementTransformer.cs
+++ b/Source/Dafny/RefinementTransformer.cs
@@ -744,14 +744,20 @@ namespace Microsoft.Dafny
               if (m.Mod.Expressions.Count != 0) {

                 reporter.Error(m.Mod.Expressions[0].E.tok, "a refining method is not allowed to extend the modifies clause");

               }

+              // If the previous method was not specified with "decreases *", then the new method is not allowed to provide any "decreases" clause.

+              // Any "decreases *" clause is not inherited, so if the previous method was specified with "decreases *", then the new method needs

+              // to either redeclare "decreases *", provided a termination-checking "decreases" clause, or give no "decreases" clause and thus

+              // get a default "decreases" loop.

               Specification<Expression> decreases;

-              if (Contract.Exists(prevMethod.Decreases.Expressions, e => e is WildcardExpr)) {

-                decreases = m.Decreases;

+              if (m.Decreases.Expressions.Count == 0) {

+                // inherited whatever the previous loop used

+                decreases = refinementCloner.CloneSpecExpr(prevMethod.Decreases);

               } else {

-                if (m.Decreases.Expressions.Count != 0) {

+                if (!Contract.Exists(prevMethod.Decreases.Expressions, e => e is WildcardExpr)) {

+                  // If the previous loop was not specified with "decreases *", then the new loop is not allowed to provide any "decreases" clause.

                   reporter.Error(m.Decreases.Expressions[0].tok, "decreases clause on refining method not supported, unless the refined method was specified with 'decreases *'");

                 }

-                decreases = refinementCloner.CloneSpecExpr(prevMethod.Decreases);

+                decreases = m.Decreases;

               }

               if (prevMethod.IsStatic != m.IsStatic) {

                 reporter.Error(m, "a method in a refining module cannot be changed from static to non-static or vice versa: {0}", m.Name);

@@ -1402,18 +1408,16 @@ namespace Microsoft.Dafny
       // the Specification structures with a null list).

       Contract.Assume(cNew.Mod.Expressions == null);

 

-      // If the previous loop was not specified with "decreases *", then the new loop is not allowed to provide any "decreases" clause.

-      // Any "decreases *" clause is not inherited, so if the previous loop was specified with "decreases *", then the new loop needs

-      // to either redeclare "decreases *", provided a termination-checking "decreases" clause, or give no "decreases" clause and thus

-      // get a default "decreases" loop.

       Specification<Expression> decr;

-      if (Contract.Exists(cOld.Decreases.Expressions, e => e is WildcardExpr)) {

-        decr = cNew.Decreases;  // take the new decreases clauses, whatever they may be (including nothing at all)

+      if (cNew.Decreases.Expressions.Count == 0) {

+        // inherited whatever the previous loop used

+        decr = refinementCloner.CloneSpecExpr(cOld.Decreases);

       } else {

-        if (cNew.Decreases.Expressions.Count != 0) {

+        if (!Contract.Exists(cOld.Decreases.Expressions, e => e is WildcardExpr)) {

+          // If the previous loop was not specified with "decreases *", then the new loop is not allowed to provide any "decreases" clause.

           reporter.Error(cNew.Decreases.Expressions[0].tok, "a refining loop can provide a decreases clause only if the loop being refined was declared with 'decreases *'");

         }

-        decr = refinementCloner.CloneSpecExpr(cOld.Decreases);

+        decr = cNew.Decreases;

       }

 

       var invs = cOld.Invariants.ConvertAll(refinementCloner.CloneMayBeFreeExpr);

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 172f63ad..d660a8e5 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -1944,9 +1944,6 @@ namespace Microsoft.Dafny
             }

           }

         }

-        if (!m.IsTailRecursive && m.Body != null && Contract.Exists(m.Decreases.Expressions, e => e is WildcardExpr)) {

-          Error(m.Decreases.Expressions[0].tok, "'decreases *' is allowed only on tail-recursive methods");

-        }

       } else if (member is Function) {

         var f = (Function)member;

         var errorCount = ErrorCount;

@@ -4825,8 +4822,12 @@ namespace Microsoft.Dafny
         ResolveAttributes(s.Decreases.Attributes, new ResolveOpts(codeContext, true));

         foreach (Expression e in s.Decreases.Expressions) {

           ResolveExpression(e, new ResolveOpts(codeContext, true));

-          if (bodyMustBeSpecOnly && e is WildcardExpr) {

-            Error(e, "'decreases *' is not allowed on ghost loops");

+          if (e is WildcardExpr) {

+            if (bodyMustBeSpecOnly) {

+              Error(e, "'decreases *' is not allowed on ghost loops");

+            } else if (!codeContext.AllowsNontermination) {

+              Error(e, "a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating");

+            }

           }

           // any type is fine

         }

@@ -4859,8 +4860,12 @@ namespace Microsoft.Dafny
 

         foreach (Expression e in s.Decreases.Expressions) {

           ResolveExpression(e, new ResolveOpts(codeContext, true));

-          if (s.IsGhost && e is WildcardExpr) {

-            Error(e, "'decreases *' is not allowed on ghost loops");

+          if (e is WildcardExpr) {

+            if (s.IsGhost) {

+              Error(e, "'decreases *' is not allowed on ghost loops");

+            } else if (!codeContext.AllowsNontermination) {

+              Error(e, "a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating");

+            }

           }

           // any type is fine

         }

@@ -5436,7 +5441,7 @@ namespace Microsoft.Dafny
         s.Method = (Method)member;

         callee = s.Method;

         if (!isInitCall && callee is Constructor) {

-          Error(s, "a constructor is only allowed to be called when an object is being allocated");

+          Error(s, "a constructor is allowed to be called only when an object is being allocated");

         }

         s.IsGhost = callee.IsGhost;

         if (specContextOnly && !callee.IsGhost) {

@@ -5561,6 +5566,9 @@ namespace Microsoft.Dafny
           }

         }

       }

+      if (callee != null && Contract.Exists(callee.Decreases.Expressions, e => e is WildcardExpr) && !codeContext.AllowsNontermination) {

+        Error(s.Tok, "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");

+      }

     }

 

     /// <summary>

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 3688ed3f..b9ad41a3 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -7956,9 +7956,6 @@ namespace Microsoft.Dafny {
         string msg;

         if (s.InferredDecreases) {

           msg = "cannot prove termination; try supplying a decreases clause for the loop";

-          if (s is RefinedWhileStmt) {

-            msg += " (note that a refined loop does not inherit 'decreases *' from the refined loop)";

-          }

         } else {

           msg = "decreases expression might not decrease";

         }

@@ -8356,6 +8353,10 @@ namespace Microsoft.Dafny {
       var types1 = new List<Type>();

       var callee = new List<Expr>();

       var caller = new List<Expr>();

+      if (RefinementToken.IsInherited(tok, currentModule) && contextDecreases.All(e => !RefinementToken.IsInherited(e.tok, currentModule))) {

+        // the call site is inherited but all the context decreases expressions are new

+        tok = new ForceCheckToken(tok);

+      }

       for (int i = 0; i < N; i++) {

         Expression e0 = Substitute(calleeDecreases[i], receiverReplacement, substMap);

         Expression e1 = contextDecreases[i];

@@ -8363,7 +8364,7 @@ namespace Microsoft.Dafny {
           N = i;

           break;

         }

-        toks.Add(tok);

+        toks.Add(new NestedToken(tok, e1.tok));

         types0.Add(e0.Type.NormalizeExpand());

         types1.Add(e1.Type.NormalizeExpand());

         callee.Add(etranCurrent.TrExpr(e0));

diff --git a/Test/VSI-Benchmarks/b8.dfy b/Test/VSI-Benchmarks/b8.dfy
index 5ab75e7a..ea1911fe 100644
--- a/Test/VSI-Benchmarks/b8.dfy
+++ b/Test/VSI-Benchmarks/b8.dfy
@@ -43,13 +43,14 @@ class Glossary {
     ensures multiset(r.contents) == multiset(old(q.contents));

 

   method Main()

+    decreases *;  // this Main method may run forever

   {

     var rs:= new ReaderStream;

     rs.Open();

     var glossary := new Map<Word,seq<Word>>.Init();

     var q := new Queue<Word>.Init();

     

-    while (true)

+    while true

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

       invariant glossary.Valid();

       invariant glossary !in rs.footprint;

@@ -60,11 +61,11 @@ class Glossary {
       decreases *;  // we leave out the decreases clause - unbounded stream

     {

       var term,definition := readDefinition(rs);

-      if (term == null) {

+      if term == null {

         break;

       }

       var present, d := glossary.Find(term);

-      if (!present) {

+      if !present {

         glossary.Add(term,definition);

         q.Enqueue(term);

       }

@@ -77,7 +78,7 @@ class Glossary {
     var wr := new WriterStream;

     wr.Create();

 

-    while (0 < |q.contents|)

+    while 0 < |q.contents|

       invariant wr.Valid() && fresh(wr.footprint);

       invariant glossary.Valid();

       invariant glossary !in wr.footprint && null !in glossary.keys;

@@ -94,7 +95,7 @@ class Glossary {
       var i := 0;

 

       var qcon := q.contents;

-      while (i < |definition|)

+      while i < |definition|

         invariant wr.Valid() && fresh(wr.footprint);

         invariant glossary.Valid();

         invariant glossary !in wr.footprint && null !in glossary.keys;

@@ -106,12 +107,9 @@ class Glossary {
         var w := definition[i];

         var d;

         present, d := glossary.Find(w);

-        if (present)

-        {

+        if present {

           wr. PutWordInsideHyperlink(w, w);

-        }

-        else 

-        {

+        } else {

           wr. PutWord(w);

         }

         i:= i +1;

@@ -126,19 +124,18 @@ class Glossary {
     modifies rs.footprint;

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

     ensures term != null ==> null !in definition;

+    decreases *;  // this method may run forever

   {

     term := rs.GetWord();

-    if (term != null)

-    {

+    if term != null {

       definition := [];

-      while (true)

+      while true

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

         invariant null !in definition;

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

       {

         var w := rs.GetWord();

-        if (w == null)

-        {

+        if w == null {

           break;

         }

         definition := definition + [w];

@@ -276,7 +273,7 @@ class Map<Key(==),Value> {
                                      keys[i] == key && values[i] == val);

   {

     var j := FindIndex(key);

-    if (j == -1) {

+    if j == -1 {

       present := false;

     } else {

       present := true;

@@ -295,7 +292,7 @@ class Map<Key(==),Value> {
     ensures key !in old(keys) ==> keys == old(keys) + [key] && values == old(values) + [val];

   {

     var j := FindIndex(key);

-    if (j == -1) {

+    if j == -1 {

       keys := keys + [key];

       values := values + [val];

     } else {

@@ -324,7 +321,7 @@ class Map<Key(==),Value> {
               values[h..] == old(values)[h+1..]);

   {

     var j := FindIndex(key);

-    if (0 <= j) {

+    if 0 <= j {

       keys := keys[..j] + keys[j+1..];

       values := values[..j] + values[j+1..];

     }

@@ -337,11 +334,11 @@ class Map<Key(==),Value> {
     ensures 0 <= idx ==> keys[idx] == key;

   {

     var j := 0;

-    while (j < |keys|)

+    while j < |keys|

       invariant j <= |keys|;

       invariant key !in keys[..j];

     {

-      if (keys[j] == key) {

+      if keys[j] == key {

         idx := j;

         return;

       }

diff --git a/Test/dafny0/DTypes.dfy b/Test/dafny0/DTypes.dfy
index 30c3eefd..70f9bbd0 100644
--- a/Test/dafny0/DTypes.dfy
+++ b/Test/dafny0/DTypes.dfy
@@ -57,6 +57,7 @@ class C {
   }

 

   method A5()

+    decreases *;

   {

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

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

diff --git a/Test/dafny0/DTypes.dfy.expect b/Test/dafny0/DTypes.dfy.expect
index fccf1c9a..9b4288e9 100644
--- a/Test/dafny0/DTypes.dfy.expect
+++ b/Test/dafny0/DTypes.dfy.expect
@@ -1,5 +1,5 @@
-DTypes.dfy(181,3): Error BP5003: A postcondition might not hold on this return path.

-DTypes.dfy(180,15): Related location: This is the postcondition that might not hold.

+DTypes.dfy(182,3): Error BP5003: A postcondition might not hold on this return path.

+DTypes.dfy(181,15): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon0

 DTypes.dfy(18,14): Error: assertion violation

@@ -8,20 +8,20 @@ Execution trace:
 DTypes.dfy(56,18): Error: assertion violation

 Execution trace:

     (0,0): anon0

-DTypes.dfy(120,13): Error: assertion violation

-DTypes.dfy(92,30): Related location

+DTypes.dfy(121,13): Error: assertion violation

+DTypes.dfy(93,30): Related location

 Execution trace:

     (0,0): anon0

-DTypes.dfy(126,13): Error: assertion violation

-DTypes.dfy(92,20): Related location

+DTypes.dfy(127,13): Error: assertion violation

+DTypes.dfy(93,20): Related location

 Execution trace:

     (0,0): anon0

-DTypes.dfy(136,12): Error: assertion violation

-DTypes.dfy(131,6): Related location

-DTypes.dfy(92,20): Related location

+DTypes.dfy(137,12): Error: assertion violation

+DTypes.dfy(132,6): Related location

+DTypes.dfy(93,20): Related location

 Execution trace:

     (0,0): anon0

-DTypes.dfy(157,12): Error: assertion violation

+DTypes.dfy(158,12): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon5_Then

diff --git a/Test/dafny0/Modules1.dfy.expect b/Test/dafny0/Modules1.dfy.expect
index dd53a883..b269e3b2 100644
--- a/Test/dafny0/Modules1.dfy.expect
+++ b/Test/dafny0/Modules1.dfy.expect
@@ -11,6 +11,7 @@ Execution trace:
     (0,0): anon0

     (0,0): anon3_Else

 Modules1.dfy(56,3): Error: decreases expression must be bounded below by 0

+Modules1.dfy(54,13): Related location

 Execution trace:

     (0,0): anon0

 Modules1.dfy(62,3): Error: failure to decrease termination measure

diff --git a/Test/dafny0/RealCompare.dfy.expect b/Test/dafny0/RealCompare.dfy.expect
index aca50548..e0f70fc0 100644
--- a/Test/dafny0/RealCompare.dfy.expect
+++ b/Test/dafny0/RealCompare.dfy.expect
@@ -3,6 +3,7 @@ Execution trace:
     (0,0): anon0

     (0,0): anon3_Then

 RealCompare.dfy(50,3): Error: decreases expression must be bounded below by 0.0

+RealCompare.dfy(48,13): Related location

 Execution trace:

     (0,0): anon0

 RealCompare.dfy(141,12): Error: assertion violation

diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index 50628438..1f604b9c 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -1114,3 +1114,41 @@ module ObjectSetComprehensions {
 

   method D() { var x := set o : object | true :: o; }

 }

+

+// ----- decreases * tests ----

+

+method NonTermination_A()

+{

+  NonTermination_B();  // error: to call a non-terminating method, the caller must be marked 'decreases *'

+}

+

+method NonTermination_B()

+  decreases *;

+{

+  while true

+    decreases *;

+  {

+  }

+}

+

+method NonTermination_C()

+{

+  while true

+    decreases *;  // error: to use an infinite loop, the enclosing method must be marked 'decreases *'

+  {

+  }

+}

+

+method NonTermination_D()

+  decreases *;

+{

+  var n := 0;

+  while n < 100  // note, no 'decreases *' here, even if the nested loop may fail to terminate

+  {

+    while *

+      decreases *;

+    {

+    }

+    n := n + 1;

+  }

+}

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

diff --git a/Test/dafny0/TailCalls.dfy b/Test/dafny0/TailCalls.dfy
index ba683679..0bc282a4 100644
--- a/Test/dafny0/TailCalls.dfy
+++ b/Test/dafny0/TailCalls.dfy
@@ -30,25 +30,24 @@ method C(q: int) returns (x: int)
 }

 

 method D(q: int) returns (x: int)

-  decreases *;  // error: not allowed, because the method is not tail recursive

 {

   x := D(q-1);

   x := x + 1;

 }

 

-method E0(q: int) returns (x: int)

-  decreases *;  // error: not allowed, because the method is not tail recursive (since mutually recursive methods are currently not recognized as being tail recursive)

+method {:tailrecursion} E0(q: int) returns (x: int)  // error: not allowed, because the method is not

+  // tail recursive (since mutually recursive methods are currently not recognized as being tail recursive)

 {

   x := E1(q-1);

 }

-method E1(q: int) returns (x: int)

-  decreases *;  // error: not allowed, because the method is not tail recursive (since mutually recursive methods are currently not recognized as being tail recursive)

+method {:tailrecursion} E1(q: int) returns (x: int)  // error: not allowed, because the method is not

+  // tail recursive (since mutually recursive methods are currently not recognized as being tail recursive)

 {

   x := E0(q);

 }

 

 method F0(q: int) returns (x: int)

-  decreases *;  // fine, but no 'decreases' spec is needed at all here

+  decreases *;  // fine

 {

   x := D(q);

 }

@@ -63,18 +62,18 @@ method {:tailrecursion} G0(q: int) returns (x: int)
 {

   x := D(q);

 }

-method {:tailrecursion false} G1(q: int) returns (x: int)

-  decreases *;  // error: even though there is no recursion in this method's body, the annotation specifically says "not tail recursive", so (the easiest thing to do in the Resolver was to) generate an error

+method {:tailrecursion false} G1(q: int) returns (x: int)  // the annotation tells the compiler not to tail-call optimize

+  decreases *;

 {

-  x := D(q);

+  x := G1(q);

 }

 

 method H0(q: int) returns (x: int)

-  decreases *;  // fine, but no 'decreases' spec is needed at all here

+  decreases *;  // fine

 method {:tailrecursion} H1(q: int) returns (x: int)

-  decreases *;  // fine, but no 'decreases' spec is needed at all here

+  decreases *;  // fine

 method H2(q: int) returns (x: int)

-  decreases 5;  // fine, but no 'decreases' spec is needed at all here

+  decreases 5;  // fine

 

 class {:autocontracts} MyAutoContractClass {

   var left: MyAutoContractClass;

diff --git a/Test/dafny0/TailCalls.dfy.expect b/Test/dafny0/TailCalls.dfy.expect
index 7fc51902..dc1eec5b 100644
--- a/Test/dafny0/TailCalls.dfy.expect
+++ b/Test/dafny0/TailCalls.dfy.expect
@@ -1,6 +1,4 @@
 TailCalls.dfy(21,15): Error: this recursive call is not recognized as being tail recursive, because it is followed by non-ghost code

-TailCalls.dfy(33,12): Error: 'decreases *' is allowed only on tail-recursive methods

-TailCalls.dfy(40,12): Error: 'decreases *' is allowed only on tail-recursive methods

-TailCalls.dfy(45,12): Error: 'decreases *' is allowed only on tail-recursive methods

-TailCalls.dfy(67,12): Error: 'decreases *' is allowed only on tail-recursive methods

-5 resolution/type errors detected in TailCalls.dfy

+TailCalls.dfy(38,24): Error: sorry, tail-call optimizations are not supported for mutually recursive methods

+TailCalls.dfy(43,24): Error: sorry, tail-call optimizations are not supported for mutually recursive methods

+3 resolution/type errors detected in TailCalls.dfy

diff --git a/Test/dafny0/Termination.dfy b/Test/dafny0/Termination.dfy
index 377865fe..70c30aa6 100644
--- a/Test/dafny0/Termination.dfy
+++ b/Test/dafny0/Termination.dfy
@@ -275,6 +275,7 @@ function Zipper2<T>(a: List<T>, b: List<T>): List<T>
 

 method WhileStar0(n: int)

   requires 2 <= n;

+  decreases *;

 {

   var m := n;

   var k := 0;

@@ -429,3 +430,22 @@ class C {
     }

   }

 }

+

+// --------------------- decreases * tests

+

+module TerminationRefinement0 {

+  method M(x: int)

+    decreases *;

+  {

+    M(x);  // error [in TerminationRefinement1]: bad recursion

+           // Note, no complaint is issued in TerminationRefinement0, since

+           // the method is declared with 'decreases *'.

+  }

+}

+module TerminationRefinement1 refines TerminationRefinement0 {

+  method M...

+    decreases 4;  // this will cause termination checking to be done, and it will produce an error message for the recursive call

+  {

+    ...;

+  }

+}

diff --git a/Test/dafny0/Termination.dfy.expect b/Test/dafny0/Termination.dfy.expect
index b050c7de..ef8ee72e 100644
--- a/Test/dafny0/Termination.dfy.expect
+++ b/Test/dafny0/Termination.dfy.expect
@@ -1,4 +1,7 @@
-Termination.dfy(359,47): Error: failure to decrease termination measure

+Termination.dfy[TerminationRefinement1](440,5): Error: failure to decrease termination measure

+Execution trace:

+    (0,0): anon0

+Termination.dfy(360,47): Error: failure to decrease termination measure

 Execution trace:

     (0,0): anon0

     (0,0): anon7_Else

@@ -44,12 +47,12 @@ Execution trace:
     (0,0): anon6_Else

     (0,0): anon7_Else

     (0,0): anon8_Then

-Termination.dfy(294,3): Error: decreases expression might not decrease

+Termination.dfy(295,3): Error: decreases expression might not decrease

 Execution trace:

-    Termination.dfy(294,3): anon9_LoopHead

+    Termination.dfy(295,3): anon9_LoopHead

     (0,0): anon9_LoopBody

-    Termination.dfy(294,3): anon10_Else

-    Termination.dfy(294,3): anon11_Else

+    Termination.dfy(295,3): anon10_Else

+    Termination.dfy(295,3): anon11_Else

     (0,0): anon12_Else

 

-Dafny program verifier finished with 59 verified, 7 errors

+Dafny program verifier finished with 62 verified, 8 errors

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

diff --git a/Test/dafny2/TreeBarrier.dfy b/Test/dafny2/TreeBarrier.dfy
index ffc75745..b6a44480 100644
--- a/Test/dafny2/TreeBarrier.dfy
+++ b/Test/dafny2/TreeBarrier.dfy
@@ -70,8 +70,8 @@ class Node {
     requires valid();

     requires before();

     modifies this, left, right;

+    decreases *;  // allow the method to not terminate

   {

-

 //A

     pc := 1;

     if(left != null) {

diff --git a/Test/vstte2012/Combinators.dfy b/Test/vstte2012/Combinators.dfy
index 82bfc970..37f3bd68 100644
--- a/Test/vstte2012/Combinators.dfy
+++ b/Test/vstte2012/Combinators.dfy
@@ -202,25 +202,25 @@ ghost method Lemma_FindAndStep(t: Term) returns (r: Term, C: Context, u: Term)
             r == EvalExpr(C, Step(u));

 {

   Lemma_ContextPossibilities(t);

-  if (Step(t) != t) {

+  if Step(t) != t {

     // t == Hole[t] and Step applies t.  So, return Hole[Step(t)]

     return Step(t), Hole, t;

-  } else if (!t.Apply?) {

+  } else if !t.Apply? {

     r := t;

   } else {

     r, C, u := Lemma_FindAndStep(t.car);  // (*)

-    if (r != t.car) {

+    if r != t.car {

       // t has the form (a b) where a==t.car and b==t.cdr, and a==C[u] for some

       // context C and some u to which the Step applies.  t can therefore be

       // denoted by (C[u] b) == (C b)[u] and the Step applies to u.  So, return

       // (C b)[Step(u)] == (C[Step(u)] b).  Note that FindAndStep(a)

       // gives C[Step(u)].

       return Apply(r, t.cdr), C_term(C, t.cdr), u;

-    } else if (IsValue(t.car)) {

+    } else if IsValue(t.car) {

       r, C, u := Lemma_FindAndStep(t.cdr);

       assert IsTerminal(t.car);  // make sure this is still remembered from (*)

 

-      if (r != t.cdr) {

+      if r != t.cdr {

         // t has the form (a b) where a==t.car and b==t.cdr and "a" is a Value,

         // and b==C[u] for some context C and some u to which the Step applies.

         // t can therefore be denoted by (a C[u]) == (C a)[u] and the Step

@@ -305,15 +305,16 @@ method reduction(t: Term) returns (r: Term)
   ensures exists trace :: IsTrace(trace, t, r);

   // The result "r" cannot be reduced any further:

   ensures IsTerminal(r);

+  decreases *;  // allow this method to diverge

 {

   r := t;

   ghost var trace := EmptyTrace;

-  while (true)

+  while true

     invariant IsTrace(trace, t, r);

     decreases *;  // allow this statement to loop forever

   {

     var u := FindAndStep(r);

-    if (u == r) {

+    if u == r {

       // we have found a fixpoint

       Theorem_FindAndStep(r);

       return;

@@ -365,13 +366,13 @@ method VerificationTask2(t: Term) returns (r: Term)
 {

   r := t;

   ghost var trace := EmptyTrace;

-  while (true)

+  while true

     invariant IsTrace(trace, t, r) && !ContainsS(r);

     invariant TerminatingReduction(t) == TerminatingReduction(r);

     decreases TermSize(r);

   {

     var u := FindAndStep(r);

-    if (u == r) {

+    if u == r {

       // we have found a fixpoint

       Theorem_FindAndStep(r);

       return;