Termination metrics in Dafny, which are declared by "decreases" clauses, are lexicographic tuples of expressions. At each recursive (or mutually recursive) call to a function or method, Dafny checks that the effective decreases clause of the
callee is strictly smaller than the effective decreases clause of the caller.
What does "strictly smaller" mean? Dafny provides a built-in well-founded order for every type and, in some cases, between types. For example, the Boolean "false" is strictly smaller than "true", the integer 78 is strictly smaller
than 102, the set {2,5} is strictly smaller than the set {2,3,5}, and for "s" of type seq<Color> where Color is some inductive datatype, the color s[0] is strictly less than s (provided s is nonempty).
What does "effective decreases clause" mean? Dafny always appends of "top" element to the lexicographic tuple given by the user. This top element cannot be syntactically denoted in a Dafny program and it never occurs as a run-time value
either. Rather, it is a fictitious value, which here I will denote \top, such that each value that can ever occur in a Dafny program is strictly less than \top. Dafny sometimes also prepends expressions to the lexicographic tuple given by the user. The effective
decreases clause is any such prefix, followed by the user-provided decreases clause, followed by \top. I said "user-provided decreases clause", but if the user completely omits a "decreases" clause, then Dafny will usually make a guess
at one, in which case the effective decreases clause is any prefix followed by the guess followed by \top. (If you're using the Dafny IDE in Visual Studio, you can hover the mouse over the name of a recursive function or method, or the "while" keyword
for a loop, to see the "decreases" clause that Dafny guessed, if any.)
Let's take a look at the kind of example where a mysterious-looking decreases clause like "Rank, 0" is useful.
Consider two mutually recursive methods, A and B:
method A(x: nat)
{
B(x);
}
method B(x: nat)
{
if x != 0 { A(x-1); }
}
To prove termination of A and B, Dafny needs to have effective decreases clauses for A and B such that:
- the measure for the callee B(x) is strictly smaller than the measure for the caller A(x), and
- the measure for the callee A(x-1) is strictly smaller than the measure for the caller B(x).
Satisfying the second of these conditions is easy, but what about the first? Note, for example, that declaring both A and B with "decreases x;" does not work, because that won't prove a strict decrease for the call from A(x) to B(x).
Here's one possibility (for brevity, I will omit the method bodies):
method A(x: nat)
decreases x, 1;
method B(x: nat)
decreases x, 0;
For the call from A(x) to B(x), the lexicographic tuple "x, 0" is strictly smaller than "x, 1", and for the call from B(x) to A(x-1), the lexicographic tuple "x-1, 1" is strictly smaller than "x, 0".
Two things to note: First, the choice of "0" and "1" as the second components of these lexicographic tuples is rather arbitrary. It could just as well have been "true" and "false", respectively, or the sets {2,3,5} and
{2,5}. Second, the keyword "decreases" often gives rise to an intuitive English reading of the declaration. For example, you might say that the recursive calls in the definition of the familiar Fibonacci function Fib(n) "decreases n". But
when the lexicographic tuple contains constants, the English reading of the declaration becomes mysterious and may give rise to questions like "how can you decrease the constant 0?". The keyword is just that--a keyword. It says "here comes a
list of expressions that make up the lexicographic tuple I want to use for the termination measure". What is important is that one effective decreases clause is compared against another one, and it certainly makes sense to compare something to a constant
(and to compare one constant to another).
We can simplify things a little bit by remembering that Dafny appends \top to the user-supplied decreases clause. For the A-and-B example, this lets us drop the constant from the decreases clause of A:
method A(x: nat)
decreases x;
method B(x: nat)
decreases x, 0;
The effective decreases clause of A is "x, \top" and the effective decreases clause of B is "x, 0, \top". These tuples still satisfy the two conditions (x, 0, \top) < (x, \top) and (x-1, \top) < (x, 0, \top). And as before, the constant
"0" is arbitrary; anything less than \top (which is any Dafny expression) would work.
Let's take a look at one more example that better illustrates the utility of \top. Consider again two mutually recursive methods, call them Outer and Inner, representing the recursive counterparts of what iteratively might be two nested loops:
method Outer(x: nat)
{
var y :| 0 <= y;
Inner(x, y);
}
method Inner(x: nat, y: nat)
{
if y != 0 {
Inner(x, y-1);
} else if x != 0 {
Outer(x-1);
}
}
Here, I'm using an assign-such-that statement in Outer to represent some computation that takes place before Inner is called. It sets "y" to some arbitrary non-negative value. In a more concrete example, Inner would do some work for each "y"
and then continue as Outer on the next smaller "x".
Using a decreases clause "x, y" for Inner seems natural, but if we don't have any bound on the size of the "y" computed by Outer, there is no expression we can write in decreases clause of Outer that is sure to lead to a strictly smaller
value for "y" when Inner is called. \top to the rescue. If we arrange for the effective decreases clause of Outer to be "x, \top" and the effective decreases clause for Inner to be "x, y, \top", then we can show the strict decreases
as required. Since \top is implicitly appended, the two decreases clauses declared in the program text can be:
method Outer(x: nat)
decreases x;
method Inner(x: nat, y: nat)
decreases x, y;
Moreover, remember that if a function or method has no user-declared decreases clause, Dafny will make a guess. The guess is (usually) the list of arguments of the function/method, in the order given. This is exactly the decreases clauses needed here. Thus,
Dafny successfully verifies the program without any explicit decreases clauses:
method Outer(x: nat)
{
var y :| 0 <= y;
Inner(x, y);
}
method Inner(x: nat, y: nat)
{
if y != 0 {
Inner(x, y-1);
} else if x != 0 {
Outer(x-1);
}
}
The ingredients are simple, but the end result may seem like magic. For many users, however, there may be no magic at all -- the end result may be so natural that the user never even has to bothered to think about that there was a need to prove termination
in the first place.
Rustan