14
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ Let me check whether I understand this. What you are asking for would give us, among other things, an algorithm which takes a program that computes a total recursive function and outputs a proof of a statement that the function is total (in the form of variant functions and proofs that they are suitable)? That sounds awfully uncomputable to me. $\endgroup$ – Andrej Bauer Aug 31 '10 at 18:48
  • $\begingroup$ Andrej, it sounds uncomputable to me too. What I'm asking for is a proof that it is uncomputable. $\endgroup$ – Radu GRIGore Sep 1 '10 at 9:12
7
$\begingroup$

One way to answer this is to consider the computational complexity of the decision problems for the classes of partial correctness and termination queries that are known to be decidable. Abstract interpretation using the polyhedral domain can infer the partial correctness annotations you mention in cases where the required annotations are conjunctions of linear inequalities. Computing the abstract post-condition is exponential in the number of variables. Then there is the overhead of finding the fixed point. See Cousot's early papers for more on this and the Apron library if you want to play with it directly.

Finding variant functions is decidable when the variant functions are linear. I couldn't find a complete characterization of the complexity of this, but "Termination of Linear Programs" by Tiwari has a section that discusses complexity. See also "A Complete Method for the Synthesis of Linear Ranking Functions" by Podelski and Rybalchenko. Also, Byron Cook has done work on leveraging abstract interpretation to help construct termination arguments. See, for example, "Ranking Abstractions" and "Variance Analyses from Invariance Analyses". These may give further insight into the relationship between partial correctness and termination.

Links:

$\endgroup$
  • 1
    $\begingroup$ I hope you don't mind my editing your answer and making the links active. $\endgroup$ – Andrej Bauer Feb 2 '11 at 8:33
4
$\begingroup$

There's an obvious reduction from necessary non-termination to partial correctness, namely:

P never terminates when started in an initial state satisfying φ iff {φ} P {false} is valid.

I am aware that this is another non-answer. Its advantage is that it is shorter than those above.

$\endgroup$
3
$\begingroup$

There's a standard technology – usually undecidable, of course – for populating your graph with its pre- and post-conditions, namely weakest liberal precondition semantics, which is a form of predicate transformer semantics that gives weakest preconditions for either satisfaction of the specification or non-termination. This essentially is a complete theory of partial correctness for such languages, and, indeed, full correctness

It's chalk and cheese deciding which of termination and partial correctness is where the hard work lies, since both are so badly undecidable. But partial correctness is tangled up with language design issues, both for program and specification languages, whilst the difficulty of termination is of a clean sort: for any theory used for proving termination there will be algorithms that terminate, but connot be proven to terminate relative to that theory. For example, computations in the pure polymorphic lambda calculus must terminate, but Peano arithmetic cannot prove this.

My impression is that the work on abstract interpretation pioneered by Patrick Cousot, has been the most dynamic in this area, but I don't pretend to be an expert.

$\endgroup$
  • $\begingroup$ I was trying to ask about the complexity of inferring variant functions. Sorry for not being clear! As a curiosity, Rustan Leino came up with an example last evening (in a pub) that strongly suggested to me that wlp doesn't work as well as wp&sp for the kind of programs I describe here. I'll have to double check when I get to a place more suitable for work :) $\endgroup$ – Radu GRIGore Aug 24 '10 at 12:34
  • $\begingroup$ @Radu: There's work been done on automatic termination proofs, with some nice work being done for Prolog. I can dig up some refs when I find time. $\endgroup$ – Charles Stewart Aug 24 '10 at 12:37

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.