The use of Hoare axioms for the verification of programs has become widely accepted. But it has also turned out that there are programming language constructs for which no adequate Hoare axiom system can be found, i.e., no axiom system which is sound and relatively complete. The present paper sketches the state of the art in characterizing these languages or constructs. First, an absolute minimum of knowledge about Hoare systems is presented, including the notion of relative completeness. The usual notion of completeness is not adequate because it depends too much on the underlying assertion language which may be too weak to express loop invariants or whose proof system may be incomplete. The next section, therefore, explains the central notion of expressibility, which guarantees the existence of invariants for loops and recursive procedures. Expressive interpretations of the assertion language are used for the formulation of relative completeness.

The next section presents some programming language constructs for which no adequate Hoare system exists. The main reason for these incompletenesses is the undecidability of the halting problem for the corresponding programming language, even for finite interpretations. The following section presents Clarke’s characterization theorem which reduces the existence of an adequate Hoare system to the existence of an effective procedure that, for an expressive, Herbrand-definable (i.e., minimal) interpretation I, will decide which partial correctness assertions are true in I when given an oracle for the theory Th(I). A reasonably complete sketch of the proof is presented. Afterwards, the two main deficiencies of this characterization theorem are discussed: (1) the proof system produced is an enumeration procedure which clearly could not be used in practice, and (2) it is not syntax-directed, which was one of the most prominent benefits of Hoare’s original system. Section 7 (which is the central part of the paper) discusses some recent research on these problems and on two further topics: the total correctness problem (it seems that some languages may have good total correctness Hoare axioms although they do not possess good partial correctness axioms), and the adequacy or power of the notion of expressibility.

The paper is very clearly written and, as a whole, is well worth reading. The publication includes a transcript of a discussion on this paper with contributions by P. Azcel (Manchester), J. V. Tucker (Leeds) and J. C. Sheperdson (Bristol).