Editing Hoare logic (section)

===Consequence rule===

:<math>\dfrac{P_1 \rightarrow P_2\quad   ,\quad   \{P_2\} S \{Q_2\}\quad   ,\quad   Q_2 \rightarrow Q_1}{\{P_1\} S \{Q_1\}}</math>

This rule allows to strengthen the precondition <math>P_2</math> and/or to weaken the postcondition <math>Q_2</math>.
It is used e.g. to achieve literally identical postconditions for the {{mono|then}} and the {{mono|else}} part.

For example, a proof of
:<math>\{0 \leq x \leq 15 \}\texttt{if}\ x<15\ \texttt{then}\ x:=x+1\ \texttt{else}\ x:=0\ \texttt{endif} \{0 \leq x \leq 15 \}</math>
needs to apply the conditional rule, which in turn requires to prove
:<math>\{0 \leq x \leq 15 \wedge x < 15 \}   x:=x+1   \{ 0 \leq x \leq 15 \}</math>, &nbsp; or simplified 
:<math>\{0 \leq x < 15 \}   x:=x+1   \{0 \leq x \leq 15 \}</math>
for the {{mono|then}} part, and
:<math>\{0 \leq x \leq 15 \wedge x \geq 15\}   x:=0   \{0 \leq x \leq 15\}</math>, &nbsp; or simplified 
:<math>\{x=15\}   x:=0   \{0 \leq x \leq 15 \}</math>
for the {{mono|else}} part.

However, the assignment rule for the {{mono|then}} part requires to choose {{mvar|P}} as <math>0\leq x \leq 15</math>; rule application hence yields
:<math>\{0 \leq x+1 \leq 15\}   x:=x+1   \{0 \leq x \leq 15\}</math>, &nbsp; which is logically equivalent to
:<math>\{-1 \leq x < 15\}   x:=x+1   \{0 \leq x \leq 15\}</math>.
The consequence rule is needed to strengthen the precondition <math>\{-1 \leq x < 15\}</math> obtained from the assignment rule to <math>\{0 \leq x < 15\}</math> required for the conditional rule.

Similarly, for the {{mono|else}} part, the assignment rule yields
:<math>\{0 \leq 0 \leq 15\}   x:=0   \{0 \leq x \leq 15\}</math>, &nbsp; or equivalently
:<math>\{\texttt{true}\}   x:=0   \{0 \leq x \leq 15\}</math>,
hence the consequence rule has to be applied with <math>P_1</math> and <math>P_2</math> being <math>\{x=15\}</math> and <math>\{\texttt{true}\}</math>, respectively, to strengthen again the precondition. Informally, the effect of the consequence rule is to "forget" that <math>\{x=15\}</math> is known at the entry of the {{mono|else}} part, since the assignment rule used for the {{mono|else}} part doesn't need that information.