Editing Hoare logic (section)

===Conditional rule===

:<math>\dfrac{\{B \wedge P\} S \{Q\}\quad,\quad \{\neg B \wedge P \} T \{Q\}}{\{P\} \texttt{if}\ B\ \texttt{then}\ S\ \texttt{else}\ T\ \texttt{endif} \{Q\}}</math>

The conditional rule states that a postcondition {{mvar|Q}} common to {{mono|then}} and {{mono|else}} part is also a postcondition of the whole {{mono|if...endif}} statement.{{sfn|Apt|Olderog|2019}} In the {{mono|then}} and the {{mono|else}} part, the unnegated and negated condition {{mvar|B}} can be added to the precondition {{mvar|P}}, respectively.
The condition, {{mvar|B}}, must not have side effects.
An example is given in the [[#Consequence_rule|next section]].

This rule was not contained in Hoare's original publication.{{sfn|Hoare|1969}}
However, since a statement 
:<math>\texttt{if}\ B\ \texttt{then}\ S\ \texttt{else}\ T\ \texttt{endif}</math>
has the same effect as a one-time loop construct
:<math>\texttt{bool}\ b:=\texttt{true};   \texttt{while}\ B\wedge b\ \texttt{do}\ S; b:=\texttt{false}\ \texttt{done};   b:=\texttt{true};   \texttt{while}\ \neg B\wedge b\ \texttt{do}\ T; b:=\texttt{false}\ \texttt{done}</math>
the conditional rule can be derived from the other Hoare rules.
In a similar way, rules for other derived program constructs, like {{mono|for}} loop, {{mono|do...until}} loop, {{mono|switch}}, {{mono|break}}, {{mono|continue}} can be reduced by [[program transformation]] to the rules from Hoare's original paper.