Termination

In Class 1 and Reading 1/2 we looked at a few variations of an indexOf function. Here is a version where Dafny proves that our implementation satisfies the specification:

method IndexOf(lst: seq<int>, elt: int) returns (res: int)
  ensures (res == -1 && elt !in lst)
          || (0 <= res < |lst| && lst[res] == elt)
{
  if |lst| == 0 {
    return -1;
  } else if lst[0] == elt {
    return 0;
  } else {
    var restidx := IndexOf(lst[1..], elt);
    return if restidx != -1 then restidx + 1 else -1;
  }
}

We saw a variety of bugs where, if we introduced them into indexOf, Dafny would catch and report them to us without having to run the code and discover those bugs at run-time. Here is the Python version of indexOf, with a different bug we did not consider at that time:

def indexOf(lst, elt):
    if len(lst) == 0:
        return -1
    elif lst[0] == elt:
        return 0
    else:
        restidx = indexOf(lst[:], elt)  # should be `lst[1:]`
        return restidx + 1 if restidx != -1 else -1

indexOf([1, 2, 3], 2)

In practice

Calling indexOf([1, 2, 3], 2) starts an unending succession of recursive calls that quickly exhausts the stack-frame bookkeeping resources that Python is willing to allocate. If we allowed the recursion to keep consuming resources, it would run our machine out of memory. If we rearranged the program a bit* and ran it in a language that supports tail-call optimization, we might be able to enjoy the true expression of its infinitely recursive definition: the function call would run forever and never terminate.

If we now make the same mistake in Dafny…

method IndexOf'(lst: seq<int>, elt: int) returns (res: int)
  ensures (res == -1 && elt !in lst)
          || (0 <= res < |lst| && lst[res] == elt)
{
  if |lst| == 0 {
    return -1;
  } else if lst[0] == elt {
    return 0;
  } else {
    var restidx := IndexOf'(lst[..], elt); // oops!
    return if restidx != -1 then restidx + 1 else -1;
  }
}

… it may not surprise you to learn that Dafny tries — and in this instance, fails — to prove termination.

In theory

Our aim is to prove that our programs will terminate on any valid input. If that sounds suspiciously like the sort of undecidable problem we mentioned in Reading 1/2 while introducing invariants, this halting problem is indeed one of the canonical examples of an undecidable problem. Therefore, Dafny puts a particular structure on the information it uses to prove termination and on how we give the system guidance if it cannot find a proof automatically. The fact that we have not talked about proving termination until now — even though Dafny has done it for every one of our functions and lemmas — demonstrates how amenable to automation it generally is for well-behaved programs.

In the context of verified software engineering, proving termination is not only a practical necessity. It also prevents us from making inferences that are untrue. For example:

lemma SuperLemma(P: int -> bool, x: int)
  ensures P(x)
{   SuperLemma(P, x);   }

lemma AnyIntIsEven(x: int)
  ensures x % 2 == 0
{   SuperLemma(x => x % 2 == 0, x);   }

If we ignore the question of SuperLemma’s termination, we can easily prove AnyIntIsEven by handing the predicate we need to be true to SuperLemma!

And:

function SuperLarge(): int
{   1 + SuperLarge()   }

method DefinitelyTotallyZero() returns (z: int)
  ensures z == 0
{   assert SuperLarge() == 1 + SuperLarge();
    assert false;
    return -9999;   }

If we ignore the question of SuperLarge’s termination, then SuperLarge() == 1 + SuperLarge() by definition, and mathematical consistency is broken !

Termination metric

The intuition for how Dafny proves termination follows from your experience developing and implementing recursive algorithms, where every recursive case must somehow reduce your problem towards a base case: the recursive call uses a shorter list, a smaller number, a grid with fewer empty spaces, etc.

Consider the execution of IndexOf([7, 8, 6], 6) with the working code:

                       calls                      calls
IndexOf([7, 8, 6], 6) ------> IndexOf([8, 6], 6) ------> IndexOf([6], 6)

In Dafny, every function invocation — that is, every single time any function is called — is associated with an arbitrary value called its termination metric.

Suppose we use natural numbers for the termination metric. The natural numbers have the property that there does not exist an infinite sequence of descending values: if and when a sequence reaches zero, there is no smaller number to descend to. If we annotate every function invocation with a natural number, then the proof obligation to show termination is very straightforward: show that every invocation has a smaller number than its caller. That’s a descending sequence, and there are no infinite descending sequences, so it must be finite.

For the example execution IndexOf([7, 8, 6], 6), there are many possible annotations that work:

  42                   calls    17                calls    5
IndexOf([7, 8, 6], 6) ------> IndexOf([8, 6], 6) ------> IndexOf([6], 6)

… or:

  3                    calls    2                 calls    1
IndexOf([7, 8, 6], 6) ------> IndexOf([8, 6], 6) ------> IndexOf([6], 6)

Compare those to the call graph of the broken code:

  n                     calls   n-1                    calls   n-2                    calls
IndexOf'([7, 8, 6], 6) ------> IndexOf'([7, 8, 6], 6) ------> IndexOf'([7, 8, 6], 6) ------> ...

… where there is no initial n we can pick such that we do not eventually run out of descending natural numbers to annotate the infinite chain of calls.

Of course we need a way to assign the termination metric for arbitrary executions of the function, which Dafny does with the keyword decreases. For example:

method IndexOf(lst: seq<int>, elt: int) returns (res: int)
  ensures (res == -1 && elt !in lst)
          || (0 <= res < |lst| && lst[res] == elt)
  decreases |lst|
{
  if |lst| == 0 {
    return -1;
  } else if lst[0] == elt {
    return 0;
  } else {
    var restidx := IndexOf(lst[1..], elt); 
    return if restidx != -1 then restidx + 1 else -1;
  }
}

With decreases |lst|, every invocation of IndexOf will be annotated with the value |lst|.

To prove that IndexOf always terminates, we need to show that every invocation has a smaller termination metric than its caller. IndexOf makes one recursive call:

method IndexOf(lst: seq<int>, elt: int) returns (res: int)
  ensures ...
  decreases |lst|
{
  if |lst| == 0 {
    ...
  } else if ... {
    ...
  } else {
    var restidx := IndexOf(lst[1..], elt); 
    ...
  }
}

So we need to prove that |lst| is always greater than |lst[1..]| when |lst| != 0. Dafny requires no further direction from us to prove this fact:

lemma Shorter(lst: seq<int>)
{   assert |lst| != 0 ==> |lst| > |lst[1..]|;   }

… and so the work of proving termination for IndexOf is done.

Well-founded order

At the beginning of this reading (and, as we said, for almost all of our previous functions and lemmas), Dafny proved termination for IndexOf without any provided decreases clause. Instead, Dafny supplied a default that empirically often works, and IndexOf is a case where it does.

The default decreases for IndexOf(lst: seq<int>, elt: int) is the two-tuple (lst, elt), which requires us to answer two questions:

1. How do we use a termination metric with values other than the natural numbers, such as seq<int>?

2. How do we use a termination metric whose values are tuples like (seq<int>, int)?

And the essence of the answer is that many types have comparison relations such that there are no infinite sequences of descending values. Our notation for this relation will be a curved greater-than ≻, which you should read as “reduces to.”

A relation ≻ is a well-founded order if it satisfies the following three properties, and these are the properties we require in order to use the relation as the basis for comparing termination metrics:

• Irreflexive: there is no x such that x ≻ x.

• Transitive: for all a, b, and c we have a ≻ b ∧ b ≻ c ⇒ a ≻ c.

• No infinite descending chain of values a, b, c, … exists such that a ≻ b ≻ c ≻ …­.

Familiar greater-than > on the natural numbers satisfies these requirements, so it worked in the sections above. But Dafny uses a built-in well-founded order that defines ≻ for other types as well.

For example…

Sequences: for values of type seq<T>, x ≻ y when y is a consecutive proper subsequence of x.

For example, [1, 2, 3, 4] ≻ [2, 3] ≻ [].

Dafny uses this relation on sequences to prove termination of IndexOf, because (for nonempty s) s[1..] is indeed a slice out of s.

Sets: for values of type set<T>, x ≻ y when y is a proper subset of x.

For example, Dafny uses this relation on sets to prove termination of this method:

method Count(strs: set<string>) returns (count: int)
{
  if strs == {} { return 0; }
  var s :| s in strs;
  count := Count(strs - {s}); // s in strs ==> strs > strs - {s}
  count := count + 1;         //  (where > is proper superset)  
}

Inductive data types: for values of inductive data types, x ≻ y when y is structurally included in x, which means that y is one of the parameters to the constructor of x or, recursively, a parameter to one of x’s parameters.

To use our arithmetic expression type Expr as an example:
Plus(Plus(Var("x"), Const(3)), Var("y")) ≻ Plus(Var("x"), Const(3)) ≻ Var("x")

If we look at FreeVars, the default decreases is simply expr:

datatype Expr = Const(value: int)
              | Var(name: string)
              | Plus(left: Expr, right: Expr)

function FreeVars(expr: Expr): set<string> {
  match expr
  case Const(_) => {}
  case Var(name) => {name}
  case Plus(left, right) =>
          FreeVars(left)    // expr == Plus(left, right) ==> expr > left
          + FreeVars(right) //  (where > is structural inclusion)       
}

FreeVars(expr) can make two recursive calls. For the call FreeVars(left), it must be the case that left is structurally included in expr. This call happens when expr == Plus(left, right), so we can see that left is indeed part of the structure of the larger expr.

We will see more examples in class 11.

Lexicographic tuples

And in class 12 we will examine the second question above and discuss how Dafny uses lexicographic tuples like IndexOf’s (seq<int>, int) for the termination metric. These are distinct from the built-in tuple type, so we will need to define ≻ on lexicographic tuples.

Summary

We’re used to thinking of nontermination as a bug for most programs, so it’s helpful that Dafny forces us to prove termination. Using functions as tools to state specifications, we further see that ruling out nontermination is crucial to maintaining logical soundness: nontermination would allow us to prove bogus properties by contradiction. Dafny includes a comprehensive treatment of (largely automated) termination proofs, which we scratched the surface of here and will continue to explore in class.