Added further assistance in coming up with decreases clauses in SCCs with co-recursive calls.

5 files changed, 61 insertions, 25 deletions

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 45ea1e83..2682938e 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -1455,6 +1455,11 @@ namespace Microsoft.Dafny {
   {

     IToken Tok { get; }

     Specification<Expression> Decreases { get; }

+    /// <summary>

+    /// The InferredDecreases property says whether or not a process was attempted to provide a default decreases

+    /// clause.  If such a process was attempted, even if the resulting decreases clause turned out to be empty,

+    /// the property will get the value "true".  This is so that a useful error message can be provided.

+    /// </summary>

     bool InferredDecreases { get; set; }

   }

   /// <summary>

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 29b4e9a3..3c4dfb55 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -364,7 +364,7 @@ namespace Microsoft.Dafny
           }

           var anyChangeToDecreases = FillInDefaultDecreases(m, true);

 

-          if (anyChangeToDecreases || m is PrefixLemma) {

+          if (anyChangeToDecreases || m.InferredDecreases || m is PrefixLemma) {

             bool showIt = false;

             if (m is Function) {

               // show the inferred decreases clause only if it will ever matter, i.e., if the function is recursive

@@ -409,7 +409,6 @@ namespace Microsoft.Dafny
       var anyChangeToDecreases = false;

       var decr = clbl.Decreases.Expressions;

       if (decr.Count == 0 || (clbl is PrefixLemma && decr.Count == 1)) {

-        var defaultAdded = false;

         // The default for a function starts with the function's reads clause, if any

         if (clbl is Function) {

           var fn = (Function)clbl;

@@ -417,7 +416,7 @@ namespace Microsoft.Dafny
             // start the default lexicographic tuple with the reads clause

             var r = FrameToObjectSet(fn.Reads);

             decr.Add(AutoGeneratedExpression.Create(r));

-            defaultAdded = true;

+            anyChangeToDecreases = true;

           }

         }

 

@@ -428,14 +427,11 @@ namespace Microsoft.Dafny
             var ie = new IdentifierExpr(p.tok, p.Name);

             ie.Var = p; ie.Type = p.Type;  // resolve it here

             decr.Add(AutoGeneratedExpression.Create(ie));

-            defaultAdded = true;

+            anyChangeToDecreases = true;

           }

         }

 

-        if (defaultAdded) {

-          clbl.InferredDecreases = true;

-          anyChangeToDecreases = true;

-        }

+        clbl.InferredDecreases = true;  // this indicates that finding a default decreases clause was attempted

       }

       if (addPrefixInCoClusters && clbl is Function) {

         var fn = (Function)clbl;

@@ -443,13 +439,13 @@ namespace Microsoft.Dafny
           case Function.CoCallClusterInvolvement.None:

             break;

           case Function.CoCallClusterInvolvement.IsMutuallyRecursiveTarget:

-            // prefix: 1,

-            clbl.Decreases.Expressions.Insert(0, Expression.CreateIntLiteral(fn.tok, 1));

+            // prefix: decreases 0,

+            clbl.Decreases.Expressions.Insert(0, Expression.CreateIntLiteral(fn.tok, 0));

             anyChangeToDecreases = true;

             break;

           case Function.CoCallClusterInvolvement.CoRecursiveTargetAllTheWay:

-            // prefix: 0,

-            clbl.Decreases.Expressions.Insert(0, Expression.CreateIntLiteral(fn.tok, 0));

+            // prefix: decreases 1,

+            clbl.Decreases.Expressions.Insert(0, Expression.CreateIntLiteral(fn.tok, 1));

             anyChangeToDecreases = true;

             break;

           default:

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 1521376e..3b0ca15b 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1389,7 +1389,7 @@ Execution trace:
     (0,0): anon0

     (0,0): anon3_Else

 

-Dafny program verifier finished with 15 verified, 8 errors

+Dafny program verifier finished with 20 verified, 8 errors

 

 -------------------- CoResolution.dfy --------------------

 CoResolution.dfy(14,9): Error: member Undeclared# does not exist in class _default

diff --git a/Test/dafny0/Corecursion.dfy b/Test/dafny0/Corecursion.dfy
index e22bbf84..3a6fc976 100644
--- a/Test/dafny0/Corecursion.dfy
+++ b/Test/dafny0/Corecursion.dfy
@@ -165,3 +165,42 @@ module FunctionSCCsWithMethods {
     var h := H();

   }

 }

+

+// --------------------------------------------------

+

+module AutomaticPrefixingOfCoClusterDecreasesClauses {

+  codatatype Stream<T> = Cons(head: T, tail: Stream)

+

+  // The following three functions will verify automatically

+  function H(): Stream<int>  // automatic:  decreases 1;

+  {

+    F(true)

+  }

+  function F(b: bool): Stream<int>  // automatic:  decreases 0, b;

+  {

+    if b then Cons(5, G()) else Cons(7, H())

+  }

+  function G(): Stream<int>  // automatic:  decreases 1;

+  {

+    F(false)

+  }

+

+  // In the following, A gets a default decreases clause of 1, because

+  // the only recursive call to A is a self-call.  B, on the other

+  // hand, has a mutually recursive call from A, and therefore it gets

+  // a decreases clause of 0.

+  function A(n: nat): Stream<int>  // automatic:  decreases 1, n;

+  {

+    if n < 100 then

+      B(n)  // the automatic decreases clauses take care of the termination of this call

+    else

+      A(n - 1)  // termination proved on account of decreasing 1,n

+  }

+  function B(n: nat): Stream<int>  // automatic:  decreases 0, n;

+  {

+    if n < 100 then

+      Cons(n, A(n + 102))  // co-recursive call, so no termination check

+    else

+      B(n - 1)  // termination proved on account of decreasing 0,n

+  }

+}

diff --git a/Test/dafny4/KozenSilva.dfy b/Test/dafny4/KozenSilva.dfy
index 9e4269b5..101ac3da 100644
--- a/Test/dafny4/KozenSilva.dfy
+++ b/Test/dafny4/KozenSilva.dfy
@@ -263,19 +263,15 @@ function merge(s: Stream, t: Stream): Stream
 // Dafny treats the call as a co-recurvie call.  A consequence of this is that

 // there is no proof obligation to show termination for that call.  However, the

 // call from SplitRight back to SplitLeft is an ordinary (mutually) recursive

-// call, and hence Dafny checks termination for it.  Dafny has some simple

-// heuristics, based on the types of the arguments of a call, for trying to

-// prove termination.  In this case, the type is a co-datatype, for which Dafny

-// does not define any useful well-founded order.  Instead, the termination

-// argument needs to be supplied explicitly in terms of a metric, rank, variant

-// function, or whatever you want to call it--"decreases" clause in Dafny.  In

-// this case, Dafny will use a "decreases \top" for SplitRight ("\top" is not

-// concrete syntax; I'm using it here just as an illustration).  From this,

-// Dafny can prove termination, because the (arbitrary non-\top) value 0 of

-// the callee is smaller than the "\top" of the caller.  (Hm, it seems that

-// Dafny could be modified to detect this case automatically.)

+// call, and hence Dafny checks termination for it.

+// In general, the termination argument needs to be supplied explicitly in terms

+// of a metric, rank, variant function, or whatever you want to call it--a

+// "decreases" clause in Dafny.  Dafny provides some help in making up "decreases"

+// clauses, and in this case it automatically adds "decreases 0;" to SplitLeft

+// and "decreases 1;" to SplitRight.  With these "decreases" clauses, the

+// termination check of SplitRight's call to SplitLeft will simply be "0 < 1",

+// which is trivial to check.

 function SplitLeft(s: Stream): Stream

-  decreases 0;

 {

   Cons(s.hd, SplitRight(s.tl))

 }