Hoare logic

Hoare logic is a formal system for proving program properties with assertions about states before and after commands. Its central notation, the Hoare triple, relates a precondition, a program, and a postcondition.

Hoare triple: A judgment stating that a command, begun in a state satisfying a precondition, ends in a state satisfying a postcondition if it terminates. This notation is the basic judgment that Hoare logic proves.
Assertion (computer science): A logical formula describing a property that should hold at a particular point in program execution. Preconditions and postconditions are assertions about program states.
Robert W. Floyd: An American computer scientist who developed an influential method for proving program properties using assertions and flowcharts. His 1967 work established a closely related foundation for deductive program verification.
Total correctness: A correctness property requiring both program termination and satisfaction of the specified postcondition. Unlike ordinary partial-correctness triples, total correctness also requires a termination proof.
Hoare logic assignment rule: An inference rule proving assignments by substituting the assigned expression into the desired postcondition. It derives the exact precondition needed to establish an assignment’s postcondition.
Program state: An assignment of values to a program’s variables at a particular point in execution. The truth of each assertion depends on the state reached by a command.
Tony Hoare: A British computer scientist who introduced the axiomatic approach to programming languages now associated with his name. His 1969 paper presented the logic’s characteristic assertion-based rules.
Operational semantics: A formal account of programming-language meaning defined through execution steps or transitions. Operational semantics describes execution directly, whereas Hoare logic reasons through assertions.
Hoare logic consequence rule: An inference rule that strengthens a precondition or weakens a postcondition using logical implication. It adapts a command’s established triple to the assertions required elsewhere in a proof.
First-order logic: A formal logic whose formulas quantify over objects and express relations among them. Its predicates and quantifiers often express program assertions.

Linked from 12 pages