Hoare logic A formalism for partial correctness proofs (see program correctness proof). Sentences have the form {p} S {q}

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.

axiomatic semantics An approach to defining the semantics of programming languages in which the meaning of a language is given by describing the true statements that can be made about programs in that language using axioms and proof rules. Typically the statements are written in some suitable formal notation, such as predicate calculus or modal logic, and concern the states before and after running the program. For example, the formula {p} S {q}

expresses: if a state satisfies property p then there is an output state after executing program S, and it satisfies property q. This assertion is called a total correctness assertion; another type is a partial correctness assertion.

The approach grew out of the early work of R. W. Floyd and C. A. R. Hoare. Though originally intended as methods for program correctness proofs (in particular as an alternative notation for the Floyd method), it was observed that Hoare logic could also be viewed as an axiomatic semantics for a very simple programming language, namely the while language. The approach was consequently extended to the description of practically useful languages.

ax·i·o·mat·ic / ˌaksēəˈmatik/ • adj. self-evident or unquestionable: it is axiomatic that dividends have to be financed. ∎  chiefly Math. relating to or containing axioms.DERIVATIVES: ax·i·o·mat·i·cal·ly / -ik(ə)lē/ adv.