A system of reasoning about programs invented by C.A.R. Hoare.

The primary concept is the Hoare Triple:


Where Precondition and Postcondition are predicates on the program state, and Code is some code. A triple states that when Precondition is true, you could execute the Code, and Postcondition would always be true. This is why {False}{False} and Magic are impossible.

There are also rules about transforming these programs. Two of these are that you may always strengthen a precondition, and that you may always weaken a postcondition.

To strengthen a statement means to reduce the set of conditions in which it will be true: A AND B is stronger than A or B (Assuming that it is always true that A is stronger than A).

To weaken a postcondition means to increase the set of states in which it is true.