Dafny: every decreases clause implicitly ends with a never-ending sequence of TOP elements; this reduces the need for manually supplied decreases clauses (see the Outer/Inner example in Test/dafny0/Termination.dfy and the Substitute/SubstSeq example in Test/dafny1/Substitution.dfy).

3 files changed, 90 insertions, 7 deletions

diff --git a/Dafny/Translator.cs b/Dafny/Translator.cs
index c64ee495..0a96a197 100644
--- a/Dafny/Translator.cs
+++ b/Dafny/Translator.cs
@@ -3035,7 +3035,12 @@ namespace Microsoft.Dafny {
       }

       return oldBfs;

     }

-        

+

+    /// <summary>

+    /// Emit to "builder" a check that calleeDecreases is less than contextDecreases.  More precisely,

+    /// the check is:

+    ///     allowance || (calleeDecreases LESS contextDecreases).

+    /// </summary>

     void CheckCallTermination(IToken/*!*/ tok, List<Expression/*!*/>/*!*/ contextDecreases, List<Expression/*!*/>/*!*/ calleeDecreases,

                               Bpl.Expr allowance,

                               Expression receiverReplacement, Dictionary<IVariable,Expression/*!*/>/*!*/ substMap,

@@ -3047,6 +3052,12 @@ namespace Microsoft.Dafny {
       Contract.Requires(etran != null);

       Contract.Requires(builder != null);

 

+      // The interpretation of the given decreases-clause expression tuples is as a lexicographic tuple, extended into

+      // an infinite tuple by appending TOP elements.  The TOP element is strictly larger than any other value given

+      // by a Dafny expression.  Each Dafny types has its own ordering, and these orderings are combined into a partial

+      // order where elements from different Dafny types are incomparable.  Thus, as an optimization below, if two

+      // components from different types are compared, the answer is taken to be false.

+

       int N = Math.Min(contextDecreases.Count, calleeDecreases.Count);

       List<IToken> toks = new List<IToken>();

       List<Type> types = new List<Type>();

@@ -3056,6 +3067,7 @@ namespace Microsoft.Dafny {
         Expression e0 = Substitute(calleeDecreases[i], receiverReplacement, substMap);

         Expression e1 = contextDecreases[i];

         if (!CompatibleDecreasesTypes(cce.NonNull(e0.Type), cce.NonNull(e1.Type))) {

+          N = i;

           break;

         }

         toks.Add(tok);

@@ -3063,7 +3075,8 @@ namespace Microsoft.Dafny {
         callee.Add(etran.TrExpr(e0));

         caller.Add(etran.TrExpr(e1));

       }

-      Bpl.Expr decrExpr = DecreasesCheck(toks, types, callee, caller, etran, builder, "", false);

+      bool endsWithWinningTopComparison = N == contextDecreases.Count && N < calleeDecreases.Count;

+      Bpl.Expr decrExpr = DecreasesCheck(toks, types, callee, caller, etran, builder, "", endsWithWinningTopComparison);

       if (allowance != null) {

         decrExpr = Bpl.Expr.Or(allowance, decrExpr);

       }

diff --git a/Test/dafny0/Termination.dfy b/Test/dafny0/Termination.dfy
index 35ff53b0..a5aca6ff 100644
--- a/Test/dafny0/Termination.dfy
+++ b/Test/dafny0/Termination.dfy
@@ -192,3 +192,75 @@ method DecreasesYieldsAnInvariant(z: int) {
   }

   assert x - y < 100;  // follows from the fact that no loop iteration increases what's in the 'decreases' clause

 }

+

+// ----------------------- top elements --------------------------------------

+

+var count: int;

+

+// Here is the old way that this had to be specified:

+

+method OuterOld(a: int)

+  modifies this;

+  decreases a, true;

+{

+  count := count + 1;

+  call InnerOld(a, count);

+}

+

+method InnerOld(a: int, b: int)

+  modifies this;

+  decreases a, false, b;

+{

+  count := count + 1;

+  if (b == 0 && 1 <= a) {

+    call OuterOld(a - 1);

+  } else if (1 <= b) {

+    call InnerOld(a, b - 1);

+  }

+}

+

+// Now the default specifications ("decreases a;" and "decreases a, b;") suffice:

+

+method Outer(a: int)

+  modifies this;

+{

+  count := count + 1;

+  call Inner(a, count);

+}

+

+method Inner(a: int, b: int)

+  modifies this;

+{

+  count := count + 1;

+  if (b == 0 && 1 <= a) {

+    call Outer(a - 1);

+  } else if (1 <= b) {

+    call Inner(a, b - 1);

+  }

+}

+

+// -------------------------- decrease either datatype value -----------------

+

+function Zipper0<T>(a: List<T>, b: List<T>): List<T>

+{

+  match a

+  case Nil => b

+  case Cons(x, c) => #List.Cons(x, Zipper0(b, c))  // error: cannot prove termination

+}

+

+function Zipper1<T>(a: List<T>, b: List<T>, k: bool): List<T>

+  decreases if k then a else b, if k then b else a;

+{

+  match a

+  case Nil => b

+  case Cons(x, c) => #List.Cons(x, Zipper1(b, c, !k))

+}

+

+function Zipper2<T>(a: List<T>, b: List<T>): List<T>

+  decreases /* max(a,b) */ if a < b then b else a,

+            /* min(a,b) */ if a < b then a else b;

+{

+  match a

+  case Nil => b

+  case Cons(x, c) => #List.Cons(x, Zipper2(b, c))

+}

diff --git a/Test/dafny1/Substitution.dfy b/Test/dafny1/Substitution.dfy
index 197d6916..8d51bdd1 100644
--- a/Test/dafny1/Substitution.dfy
+++ b/Test/dafny1/Substitution.dfy
@@ -55,7 +55,7 @@ datatype Expression {
 }

 

 static function Substitute(e: Expression, v: int, val: int): Expression

-  decreases e, true;

+  decreases e;

 {

   match e

   case Const(c) => e

@@ -66,7 +66,7 @@ static function Substitute(e: Expression, v: int, val: int): Expression
 static function SubstSeq(/*ghost*/ parent: Expression,

                          q: seq<Expression>, v: int, val: int): seq<Expression>

   requires (forall a :: a in q ==> a < parent);

-  decreases parent, false, q;

+  decreases parent, q;

 {

   if q == [] then [] else

   SubstSeq(parent, q[..|q|-1], v, val) + [Substitute(q[|q|-1], v, val)]

@@ -74,7 +74,6 @@ static function SubstSeq(/*ghost*/ parent: Expression,
 

 static ghost method TheoremSeq(e: Expression, v: int, val: int)

   ensures Substitute(Substitute(e, v, val), v, val) == Substitute(e, v, val);

-  decreases e, true;

 {

   match e {

     case Const(c) =>

@@ -100,8 +99,7 @@ static ghost method TheoremSeq(e: Expression, v: int, val: int)
   }

 }

 

-static ghost method LemmaSeq(ghost parent: Expression, ghost q: seq<Expression>,

-                                    v: int, val: int)

+static ghost method LemmaSeq(ghost parent: Expression, ghost q: seq<Expression>, v: int, val: int)

   requires (forall a :: a in q ==> a < parent);

   ensures |SubstSeq(parent, q, v, val)| == |q|;

   ensures (forall k :: 0 <= k && k < |q| ==>