 Hoare logic

Hoare logic proves properties of programs through Hoare triples $\{P\}C\{Q\}$. A precondition $P$ constrains initial states and a postcondition $Q$ constrains returned states. The basic rules establish partial correctness; termination requires a further argument.^[ref]

For a program expression $E$ whose evaluation is defined and has no side effects, the assignment rule isThe substitution replaces the free occurrences of $x$ in the desired postcondition. For example, obtaining $x\ge 1$ after x := x+1 requires $x+1\ge 1$ beforehand, so $x\ge 0$ suffices. Integer overflow must be excluded or handled by the stated arithmetic model.

Sequential composition joins a first postcondition to the next precondition. For a while loop, proving $\{I\wedge b\}C\{I\}$ establishesHere $I$ is the loop invariant. For while x > 0 do x := x-1, starting with an exact nonnegative integer, $x\ge 0$ is preserved and the false exit guard yields $x=0$. The decreasing nonnegative integer $x$ is also a loop variant, establishing total correctness for this example.^[ref]