An Introduction to Hoare Logic

Hoare logic is a formal system for reasoning about Hoare-style correctness formulae. It originates from C. A. R. Hoare's 1969 paper “An axiomatic basis for computer programming” [Hoa69], which introduces an axiomatic method for proving programs correct. Hoare logic can be viewed as the structural analysis of R. W. Floyd's semantically based inductive assertion method. Hoare's approach has received a great deal of attention ever since its introduction, and has had a significant impact on methods both for designing and verifying programs. It owes its success to three factors: (i) The first factor, which it shares with the inductive assertion method, is its universality: it is state-based, characterizes programming constructs as transformers of states, and therefore applies in principle to every such construct. (ii) The second factor in its success is its syntax directedness: every rule for a composed programming construct reduces proving properties of that construct to proving properties of its constituent constructs. In case the latter are also formulated as Hoare style correctness formulae — when characterizing parallelism this is not always the case — Hoare logic is even compositional: proving Hoare style correctness formulae for composed constructs is reduced to proving Hoare style correctness formulae for their constituent constructs without any additional knowledge about the latter's implementation. Hoare's 1969 logic is compositional. Compositional Hoare logics can also be regarded as design calculi. In such a design calculus a proof rule is interpreted as a design rule, in which a specific design goal, that of developing a program satisfying certain properties, is reduced to certain subgoals (and, in general, the satisfaction of certain verification conditions), obtained by reading that rule upside-down.