CONCEPT
Hoare Logic
C.A.R. Hoare's 1969 axiomatic system for reasoning about programs — the formal machinery behind Dijkstra's insistence on provable correctness.
Hoare logic is the formal system introduced by C.A.R. Hoare in his 1969 paper "An Axiomatic Basis for Computer Programming" that gives precise meaning to the claim that a program is correct. It uses triples of the form {P} S {Q} — where P is a precondition, S is a program fragment, and Q is a postcondition — and provides inference rules that allow the programmer to derive the correctness of compound programs from the correctness of their parts. Hoare logic is the technical foundation of provable correctness and the backbone of Dijkstra's own predicate transformer semantics. Without Hoare logic, the phrase "program correctness" has no precise meaning; with it, correctness becomes a claim that can be stated, proved, and mechanically checked.
In The You On AI Field Guide
The triple {P} S {Q} reads: "if P holds before the execution of S, and S terminates, then Q holds after." The precondition P specifies the assumptions under which the program is intended to operate; the postcondition Q specifies the property the program is