Editing Hoare logic (section)

===While rule===

:<math>\dfrac{\{P \wedge B\} S \{P\}}{\{P\} \texttt{while}\ B\ \texttt{do}\ S\ \texttt{done} \{\neg B \wedge P\}}</math>

Here {{mvar|P}} is the [[loop invariant]], which is to be preserved by the loop body {{mvar|S}}.
After the loop is finished, this invariant {{mvar|P}} still holds, and moreover <math>\neg B</math> must have caused the loop to end.
As in the conditional rule, {{mvar|B}} must not have side effects.

For example, a proof of 
:<math>\{x \leq 10\} \texttt{while}\ x<10\ \texttt{do}\ x:=x+1\ \texttt{done} \{\neg x < 10 \wedge x \leq 10\}</math>
by the while rule requires to prove
:<math>\{x \leq 10 \wedge x < 10\}   x := x + 1   \{x \leq 10 \}</math>, &nbsp; or simplified
:<math>\{x < 10\}   x := x + 1   \{x \leq 10 \}</math>,
which is easily obtained by the assignment rule.
Finally, the postcondition <math>\{\neg x <10 \wedge x\leq 10\}</math> can be simplified to <math>\{x=10\}</math>.

For another example, the while rule can be used to formally verify the following strange program to compute the exact square root {{mvar|x}} of an arbitrary number {{mvar|a}}—even if {{mvar|x}} is an integer variable and {{mvar|a}} is not a square number:
:<math>\{\texttt{true}\}   \texttt{while}\ x\cdot x \neq a\ \texttt{do}\ \texttt{skip}\ \texttt{done}   \{x \cdot x = a \wedge \texttt{true}\}</math>
After applying the while rule with {{mvar|P}} being {{mono|true}}, it remains to prove
:<math>\{\texttt{true} \wedge x\cdot x \neq a\}   \texttt{skip}   \{\texttt{true}\}</math>,
which follows from the skip rule and the consequence rule.

In fact, the strange program is ''partially'' correct: if it happened to terminate, it is certain that {{mvar|x}} must have contained (by chance) the value of {{mvar|a}}'s square root.
In all other cases, it will not terminate; therefore it is not ''totally'' correct.