“Attempts to extend Hoare’s logic to languages with goto statements have run into considerable difficulties. The proof rule proposed by Clint and Hoare [1] operates not on Hoare triples :9I p :9I S :9I q :9I but an assertions of the form :G a :9I :9I where :G a , :9I are Hoare triples . . . . de Bruin [2] interprets a variant of the Clint-Hoare system using an infinite family of truth definitions (each representating validity with respect to a set of label invariants). . . . Goto statements can be handled in a very simple and natural way if programs are represented by flowcharts. . . as in the classical paper by Floyd [3],” or if they are “annotated” (Constable and O’Donnell) [4]. Assertions are inserted as comments. A goto statement connects two points of a program charactrized by the same assertion. “Traditionally, annotated programs are viewed as informal proof outlines which can be used to develop complete proofs in Hoare’s logic.” In this paper, the author adapts the syntax of annotated programs to the system of de Bruin, and shows that the new system is equivalent to de Bruin’s.

From the theoretical point of view, this paper answers an important question; the goto statements do not change the way in which programs can be proved correct. From the practical point of view, this paper confirms the fact that annotating programs by insertion of assertions as comments is the only way to write readable, provable programs. It is well known that a program should be derived from its assertions, and that the design of a loop should start with the proposal of its invariant. As a programmer, I always assumed that the result presented in this paper was true. Now, I know it is true.

--J. Arsac, Paris, France