Question

Is there a simple way to prove the termination of a recursive function?

Here is an example function:

datatype Dummy = State1 | State2

function WalkState(str: string, s: Dummy): string {
  if str == [] then []
  else if s.State1? then WalkState(str[1..], Dummy.State2)
  else WalkState(str, Dummy.State1)
}

Answer

In general, to prove termination of any recursive structure, one needs to declare a (well-founded) measure that decreases on each iteration or recursive invocation; because a well-founded measure has no infinitely decreasing sequences, the recursion must eventually terminate. In many cases, Dafny will deduce a satisfactory (provable) measure to apply by default. But where it cannot, the user must supply such a measure. A user-supplied measure is declared in a decreases clause. Such a measure is a sequence of expressions, ordered lexicographically by the termination metric for each data type; the details of the ordering are explained in the reference manual section on Decreases Clause.

In the case of this example, the measure must be a combination of the length of the string, which decreases (and is bounded by 0) in the else if branch and the state, creating a measure in which Dummy.State1 is less than Dummy.State2 and so decreases in the final else branch. So we can write

datatype Dummy = State1 | State2

function WalkState(str: string, s: Dummy): string 
  decreases |str|, if s.State2? then 1 else 0
{
  if str == [] then []
  else if s.State1? then WalkState(str[1..], Dummy.State2)
  else WalkState(str, Dummy.State1)
}

which then proves without further user guidance.