= Solution
For a proposed <loop invariant> $I$, initial condition $P$, guard $B$, body $S$, and <postcondition> $Q$, establish these <Hoare logic> obligations:
$$
P\Rightarrow I,\qquad \{I\land B\}\ S\ \{I\},\qquad
I\land\neg B\Rightarrow Q.
$$
The first establishes $I$ before the loop; the second preserves it after each iteration; the third derives the desired result when the guard is false. Together they prove \b[<partial correctness>]. For \b[<total correctness>], also prove <algorithm termination>, for example by a nonnegative <integer> <loop variant> that strictly decreases whenever the body executes. The <loop invariant> need not be the <postcondition>: it generally describes completed and unfinished work together.
Back to article page
