To define the proof rule for the while loop we resort to the concept of a loop invariant. A loop invariant is an assertion that holds true before and after the execution of a loop body. Hence, if some assertion \(I\) is a loop invariant, it will also hold before the loop was entered and after the loop was left (if it was left at all). This gives rise to the following proof rule:
\begin{equation*}
\begin{prooftree}
\AxiomC{$\vdash\hoare{I\land e}s{I}$}
\LeftLabel{[While]}
\UnaryInfC{$\vdash\hoare{I}{\CWhile es}{I\land\neg e}$}
\end{prooftree}
\end{equation*}
The premise expresses that \(I\) must be a loop invariant. Note that we can strengthen the precondition because whenever \(s\) is executed, \(e\) also holds. In a similar way we know that as soon as we have left the loop, \(e\) will be false, hence we can stipulate the postcondition \(I\land\neg e\text{.}\)
Example 7.4.7.
Let us consider an example here as well. We subtract \(\CVar y\) from \(\CVar x\) until \(\CVar x\) becomes less than \(\CVar y\text{.}\) At the same time, we count how many times we subtracted \(\CVar y\) in \(q\text{.}\) In the end, \(\CVar q\) is the quotient of \(\CVar x\) divided by \(\CVar y\) and \(\CVar x\) contains the remainder.
\begin{equation*}
\begin{prooftree}
\AxiomC{}
\RightLabel{[Assign]}
\UnaryInfC{$\vdash\hoare{P}{\CAssnVV q0}{I}$}
\AxiomC{$\mathsf{Tree}_W$}
\RightLabel{[SeqS]}
\BinaryInfC{$\vdash\hoare{\underbrace{X=x}_{=P}}{\CAssnVV q0 \underbrace{\CWhile {\CVar x\geq \CVar y} {\CBlock{\CAssign{\CVar x}{\CVar x-\CVar y}\CAssign{\CVar q}{\CVar q+\CConst 1}}}}_{\eqdef W}}{\underbrace{\underbrace{\CVar q\cdot \CVar y+\CVar x=\CVar X}_{=I}\land \CVar x\lt \CVar y}_{=Q}}$}
\end{prooftree}
\end{equation*}
For better readability, we split off a part of the proof tree into a separate part designated by \(\mathsf{Tree}_W\text{.}\)
\begin{equation*}
\begin{prooftree}
\AxiomC{$I\land \CVar x\geq \CVar y\Rightarrow R[\CVar x-\CVar y/\CVar x]$}
\AxiomC{}
\RightLabel{[Assign]}
\UnaryInfC{$\vdash\hoare{R[\CVar x-\CVar y/\CVar x]}{\CAssign{\CVar x}{\CVar x-\CVar y}}{R}$}
\RightLabel{[Csq]}
\BinaryInfC{$\vdash\hoare{I\land \CVar x\geq \CVar y}{\CAssign{\CVar x}{\CVar x-\CVar y}}{R}$}
\AxiomC{}
\RightLabel{[Assign]}
\UnaryInfC{$\vdash\hoare{R}{\CAssign{\CVar q}{\CVar q+\CConst 1}}{I}$}
\RightLabel{[SeqS]}
\BinaryInfC{$\vdash\hoare{I \land \CVar x\geq \CVar y}{\CAssign{\CVar x}{\CVar x-\CVar y}\CAssign{\CVar q}{\CVar q+\CConst 1}}{I}$}
\RightLabel{[Block]}
\UnaryInfC{$\vdash\hoare{I \land \CVar x\geq \CVar y}{\CBlock{\CAssign{\CVar x}{\CVar x-\CVar y}\CAssign{\CVar q}{\CVar q+\CConst 1}}}{I}$}
\RightLabel{[While]}
\UnaryInfC{$\vdash\hoare{I}{W}{I\land \CVar x \lt \CVar y}$}
\end{prooftree}
\end{equation*}
For the correctness proof, we need to remember the original value of \(x\) with a ghost variable. The invariant \(\CVar q\cdot \CVar y + \CVar x = \CVar X\) is conveniently also the postcondition of the program together with the fact that the remainder is smaller than the divisor. Therefore, we do not need the consequence rule for the while loop.
Let us go through the proof from right to left. After the loop, the condition is false. Therefore, we know \(\CVar x\lt \CVar y\text{.}\) It remains to show that the invariant \(\CVar q\cdot \CVar y + \CVar x = \CVar X\) is true before the loop was entered and in each iteration of the loop. We can do this by using the [While] rule.
Before and after each iteration of the loop, \(\CVar q\) contains the count of how many times we subtracted \(\CVar y\) from \(\CVar x\text{.}\) In the loop, we subtract \(\CVar y\) from \(\CVar x\) one additional time and increase \(\CVar q\) by one. By doing this, we invalidate that invariant for a moment in the loop body but restore it afterward before reaching the end of the loop body. The intermediate condition \(R\) is true at the point before \(\CVar q\) is increased but after \(\CVar y\) is subtracted from \(\CVar x\text{.}\)
\begin{gather*}
R = I[\CVar q+1/\CVar q] = (\CVar q\cdot \CVar y + \CVar x + \CVar y = \CVar X)
\end{gather*}
By applying the [Assign] rule to \(R\text{,}\) we get the back to the invariant:
\begin{gather*}
I = R[\CVar x-\CVar y/\CVar x] = (\CVar q\cdot \CVar y + \CVar x - \CVar y + \CVar y = \CVar X) = (\CVar q \cdot \CVar y +\CVar x = \CVar X)
\end{gather*}
Lastly, it remains to show that the invariant was satisfied before the loop was entered. This is done by using the [Assign] rule for the first assignment.
\begin{gather*}
P = I[\CConst 0/\CVar q] = (\CConst 0\cdot \CVar y + \CVar x = \CVar X) = (\CVar x = \CVar X)
\end{gather*}
Prove that the remainder is non-negative for a non-negative \(x\text{.}\)
Do you need the pre-condition \(\CConst 0\lt \CVar y\text{?}\) Why or why not?