A system of reasoning about
programs invented by
C.A.R. Hoare.
The primary concept is the Hoare Triple:
{Precondition}Code{Postcondition}
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.