= Hoare logic
{c}
{wiki}
<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.<An Axiomatic Basis for Computer Programming by Tony Hoare>[sections 3–4]{ref}
For a <program expression> $E$ whose evaluation is defined and has no <side effects>, the assignment rule is
$$
\{Q[E/x]\}\ x:=E\ \{Q\}.
$$
The <substitution> replaces the free occurrences of $x$ in the desired <postcondition>. For example, obtaining $x\geq1$ after `x := x+1` requires $x+1\geq1$ beforehand, so $x\geq0$ 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\land b\}\ C\ \{I\}$ establishes
$$
\{I\}\ \mathtt{while}\ b\ \mathtt{do}\ C\ \{I\land\neg b\}.
$$
Here $I$ is the <loop invariant>. For `while x > 0 do x := x-1`, starting with an exact nonnegative <integer>, $x\geq0$ 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.<An Axiomatic Basis for Computer Programming by Tony Hoare>[sections 3.1–3.4; independent increment/countdown examples]{ref}
Back to article page
