Editing Hoare logic (section)

===While rule for total correctness===

If the [[#While_rule|above ordinary while rule]] is replaced by the following one, the Hoare calculus can also be used to prove [[total correctness]], i.e. termination as well as partial correctness. Commonly, square brackets are used here instead of curly braces to indicate the different notion of program correctness.

:<math>\dfrac{<\ \text{is a well-founded ordering on the set}\ D\quad,\quad [P \wedge B \wedge t \in D \wedge t = z]   S   [P \wedge t \in D \wedge t < z ]}{[P \wedge t \in D]   \texttt{while}\ B\ \texttt{do}\ S\ \texttt{done}   [\neg B \wedge P \wedge t \in D]}</math>

In this rule, in addition to maintaining the loop invariant, one also proves [[termination proof|termination]] by way of an expression {{mvar|t}}, called the [[loop variant]], whose value strictly decreases with respect to a [[well-founded relation]] {{mvar|<}} on some domain set {{mvar|D}} during each iteration. Since {{mvar|<}} is well-founded, a strictly decreasing [[chain (order theory)|chain]] of members of {{mvar|D}} can have only finite length, so {{mvar|t}} cannot keep decreasing forever. (For example, the usual order {{mvar|<}} is well-founded on positive [[integer]]s <math>\mathbb{N}</math>, but neither on the integers <math>\mathbb{Z}</math> nor on [[positive real numbers]] <math>\mathbb{R}^+</math>; all these sets are meant in the mathematical, not in the computing sense, they are all infinite in particular.)

Given the loop invariant {{mvar|P}}, the condition {{mvar|B}} must imply that {{mvar|t}} is not a [[minimal element]] of {{mvar|D}}, for otherwise the body {{mvar|S}} could not decrease {{mvar|t}} any further, i.e. the premise of the rule would be false. (This is one of various notations for total correctness.)
{{#tag:ref| Hoare's 1969 paper didn't provide a total correctness rule; cf. his discussion on p.579 (top left). For example Reynolds' textbook{{sfn|Reynolds|2009}} gives the following version of a total correctness rule: <math>\dfrac{P \wedge B \rightarrow 0\leq t\quad ,\quad   [P \wedge B \wedge t=z] S [P \wedge t<z]}{[P] \texttt{while}\ B\ \texttt{do}\ S\ \texttt{done} [P \wedge \neg B]}</math>  when {{mvar|z}} is an integer variable that doesn't occur free in {{mvar|P}}, {{mvar|B}}, {{mvar|S}}, or {{mvar|t}}, and {{mvar|t}} is an integer expression (Reynolds' variables renamed to fit with this article's settings). |group=note}}

Resuming the first example of the [[#While_rule|previous section]], for a total-correctness 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>
the while rule for total correctness can be applied with e.g. {{mvar|D}} being the non-negative integers with the usual order, and the expression {{mvar|t}} being  <math>10 - x</math>, which then in turn requires to prove
:<math>[x \leq 10 \wedge x < 10 \wedge 10-x \geq 0 \wedge 10-x = z] x:= x+1 [x \leq 10 \wedge 10-x \geq 0 \wedge 10-x < z]</math>
Informally speaking, we have to prove that the distance <math>10-x</math> decreases in every loop cycle, while it always remains non-negative; this process can go on only for a finite number of cycles.

The previous proof goal can be simplified to
:<math>[x < 10 \wedge 10-x = z]   x:=x+1   [x \leq 10 \wedge 10-x < z]</math>,
which can be proven as follows:
:<math>[x+1 \leq 10 \wedge 10-x-1 < z]   x:=x+1   [x \leq 10 \wedge 10-x < z]</math> is obtained by the assignment rule, and 
:<math>[x+1 \leq 10 \wedge 10-x-1 < z]</math> can be strengthened to <math> [x < 10 \wedge 10-x = z]</math> by the consequence rule.

For the second example of the [[#While_rule|previous section]], of course no expression {{mvar|t}} can be found that is decreased by the empty loop body, hence termination cannot be proved.