Hoare logic

Hoare logic is a formal system[?] developed by the British computer scientist C. A. R. Hoare, and published in his 1969 paper "An axiomatic basis for computer programming". The purpose of the system is to provide a set of logical rules which one can use to reason about computer programs.

Let C be a line, or sequence of lines, in a computer program, and let P and Q be logical predicates such that if P is true before C is executed then Q will necessarily be true after C is executed. Then the following expression

{P} C {Q}

is an expression in Hoare logic, also known as a Hoare triple. Note that if C does not terminate, then there is no "after", so Q can be any statement at all.

See also:

• Design by contract

Further reading

• C. A. R. Hoare. "An axiomatic basis for computer programming (http://doi.acm.org/10.1145/363235.363259)". Communications of the ACM, 12(10):576-585, October 1969. (Copy of the paper on the ACM website.)