If you are familiar with program verification you are likely to prefer reading the Question before the Background. If you are not familiar with program verification then you may still be able to answer this question, but you are likely to prefer reading the Background first.
Background
It is often stated that checking partial correctness is undecidable. For the sake of discussion, let's pick one very particular way of making this statement precise, in the style of Floyd--Hoare. A flowgraph is a digraph with a distinguished initial node from which all nodes are reachable. A program is a flowgraph whose nodes are commands. There are three types of commands (1) assumptions assume q, (2) assertions assert q, and (3) assignments v:=e. Here q is a fol (first-order logic) formula, e is a fol term, and v is a variable.
We say that a program is partially correct when there is a way to annotate each node x with a precondition a(x) and a postcondition b(x) such that (1) the precondition of the initial node is valid, (2) {a(x)} x {b(x)} holds for all commands x, and (3) (b(x) implies a(y)) is valid for all edges from x to y. Here the Hoare triples are defined as follows:
- {p} assert q {r} means that (p implies (q and r)) is valid
- {p} assume q {r} means that ((p and q) implies r) is valid
- {p} v:=e {r} means that ((p with e substituted for v) implies r) is valid
Here's a hand-wavy argument of why checking this partial correctness is undecidable: Once you fill in some a(x) and some b(x) you need to check if some fol formulas are valid, and that is undecidable.
A typical way to encode termination in partial correctness is to add some special assertions that essentially say "since last time I was executed, there was progress towards termination." These progress assertions must be placed such that all infinite walks on the flowgraph (that start at the initial node) contain infinitely many progress assertions. To be more specific, let's say that progress assertions always have the form assert u < v, where u and v are positive integers, are preceded by the assignment u:=f, and are followed by the assignment v:=u. Here f is a variant function, u is its current value, and v is its former value. Now, since we talk about "positive integers" and we compare them, we need to ensure that a bit more than fol is available: Let's say Peano arithmetic is available. (I don't feel strongly about this choice. Feel free to disregard if convenient.) Of course, f may use any other functions and constants that are mentioned in the program. (Note that adding assumptions at the beginning of the program is equivalent to introducing non-logical axioms.)
Now, if the program with progress assertions is still partially correct, then we know that the original program terminates.
Question
Given a terminating program, it feels that coming up with variant functions for progress assertions is hard. But how hard? (I know that even with the huge background above, I still left this question sort of open-ended, or ill-defined, depending on how you want to look at it.)
To put it differently: I'm looking for a reference that formalizes the problem of reducing termination to partial correctness and then says something about its complexity. An answer that does all this would of course be welcome.
