A formalism for partial correctness proofs (see program correctness proof). Sentences have the form

where p and q are assertions and S is a program. The meaning of such a sentence is that, starting from a state in which p is true, if S terminates it will result in a state in which q is true; p is a precondition and q is a postcondition for S. A Hoare logic for a particular programming language comprises a system of axioms and rules for deducing such sentences from other simpler ones. By repeated use of these rules it is possible ultimately to derive facts about an entire program, starting from facts about its smallest constituents. Like the Floyd method however, the approach requires judicious choice of loop invariants. As another application, Hoare logics can be taken as axiomatic semantics for programming languages. The theory of Hoare logic is determined by the assertion language for writing the pre- and postconditions (such as predicate logic) and the programming language (such as while programs). Many remarkable insights into program correctness have been obtained from the mathematical study of Hoare logic.