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

3 files changed, 48 insertions, 13 deletions

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

 }