Now, we will consider the rules for conditional statements, also called if-then or if-then-else.
Definition 20.1. $$\frac{\llparenthesis \varphi \wedge B \rrparenthesis C_1 \llparenthesis \psi \rrparenthesis \quad \llparenthesis \varphi \wedge (\neg B) \rrparenthesis C_2 \llparenthesis \psi \rrparenthesis}{\llparenthesis \varphi \rrparenthesis \text{ if ($B$) $\{C_1\}$ else $\{C_2\}$ } \llparenthesis \psi \rrparenthesis } \text{(if-then-else)}$$ $$\frac{\llparenthesis \varphi \wedge B \rrparenthesis C_1 \llparenthesis \psi \rrparenthesis \quad \llparenthesis (\varphi \wedge (\neg B)) \rightarrow \psi \rrparenthesis}{\llparenthesis \varphi \rrparenthesis \text{ if ($B$) $\{C\}$ } \llparenthesis \psi \rrparenthesis } \text{(if-then)}$$
Again, it is helpful to think of this rule in reverse. If we want to show that when executing an if-whatever block in a state satisfying $\varphi$ will result in a state satisfying $\psi$, then we need to show that the program will get to such a state whether or not our boolean condition $B$ was true.
So if $B$ was true, then $C_1$ gets executed and we need to show that $\psi$ is satisfied. But if $B$ wasn't true (i.e. $(\neg B)$ is true), then $C_2$ gets executed, but we also need to show that the program enters a state in which $\psi$ is satisfied.
We observe that the rule if-then-else is the general form of the rule. The if-then rule can be written as an if-then-else rule, but with the else empty. To see this, an if-then-else would be annotated in the following way.
| $\llparenthesis P \rrparenthesis$ | |
if (B) { | |
| $\quad \llparenthesis P \wedge B \rrparenthesis$ | if-then-else |
| $\quad C_1$ | |
| $\quad \llparenthesis Q \rrparenthesis$ | (justification) |
} else { | |
| $\quad \llparenthesis P \wedge (\neg B) \rrparenthesis$ | if-then-else |
| $\quad C_2$ | |
| $\quad \llparenthesis Q \rrparenthesis$ | (justification) |
} | |
| $\llparenthesis Q \rrparenthesis$ | if-then-else |
On the other hand, we have for if-then:
| $\llparenthesis P \rrparenthesis$ | |
if (B) { | |
| $\quad \llparenthesis P \wedge B \rrparenthesis$ | if-then |
| $\quad C$ | |
| $\quad \llparenthesis Q \rrparenthesis$ | (justification) |
} | |
| $\llparenthesis Q \rrparenthesis$ | if-then, implied: $(P \wedge (\neg B)) \rightarrow Q$. |
To push a postcondition $\psi$ back through an if statement of the form if($B$) $C_1$ else $C_2$, we push it through each of the blocks $C_1$ and $C_2$, yielding
$$\llparenthesis \varphi_1 \rrparenthesis C_1 \llparenthesis \psi \rrparenthesis \quad \llparenthesis \varphi_2 \rrparenthesis C_2 \llparenthesis \psi \rrparenthesis.$$
Example 20.2. Below is a proof for partial correctness.
| $\llparenthesis \texttt{T} \rrparenthesis$ | |
if (max < x) { | |
| $\quad \llparenthesis \texttt{T} \wedge (\max \lt x) \rrparenthesis$ | if-then |
| $\quad \llparenthesis (x \geq x) \rrparenthesis$ | implied |
$\quad$ max = x; | |
| $\quad \llparenthesis \max \geq x \rrparenthesis$ | assignment |
} | |
| $\llparenthesis \max \geq x \rrparenthesis$ | if-then implied: $(\texttt{T} \wedge (\neg (\max \lt x))) \rightarrow (\max \geq x)$ |
Generally, completing a verification proof involves the following steps: applying the appropriate inference rules, pushing assertions backwards through the program, and proving any necessary implications. The first two steps are pretty straightforward, as long as you apply the inference rules correctly; there is not much room for creativity here.
Where things may become less obvious is when proving some of the implications. To see the first implication, we just need to observe that $x \geq x$ is always true, so $\emptyset \vdash ((\texttt{T} \wedge (\max \lt x)) \rightarrow (x \geq x))$ holds.
For the second implication, we have $\emptyset \vdash ((\texttt{T} \wedge (\neg (\max \lt x))) \rightarrow (\max \geq x))$. We just observe that $(\texttt{T} \wedge (\neg (\max \lt x)))$ is equivalent to $(\neg (\max \lt x))$ and then argue that $(\neg (\max \lt x))$ is the same as $(\max \geq x)$.
Example 20.3. The following is a slightly more complex version of the previous example because we have an else block to deal with. However, we just need to stick to the prescribed procedure.
| $\llparenthesis \texttt{T} \rrparenthesis$ | |
if (x > y) { | |
| $\quad \llparenthesis x \gt y \rrparenthesis$ | if-then-else |
| $\quad \llparenthesis (((x \gt y) \wedge (x = x)) \vee ((x \leq y) \wedge (x = y))) \rrparenthesis$ | implied |
$\quad$ max = x; | |
| $\quad \llparenthesis (((x \gt y) \wedge (\max = x)) \vee ((x \leq y) \wedge (\max = y))) \rrparenthesis$ | assignment |
} else { | |
| $\quad \llparenthesis \neg(x \gt y) \rrparenthesis$ | if-then-else |
| $\quad \llparenthesis (((x \gt y) \wedge (y = x)) \vee ((x \leq y) \wedge (y = y))) \rrparenthesis$ | implied |
$\quad$ max = y; | |
| $\quad \llparenthesis (((x \gt y) \wedge (\max = x)) \vee ((x \leq y) \wedge (\max = y))) \rrparenthesis$ | assignment |
} | |
| $\llparenthesis (((x \gt y) \wedge (\max = x)) \vee ((x \leq y) \wedge (\max = y))) \rrparenthesis$ | if-then-else |
For the first implication, $\emptyset \vdash (x \gt y) \rightarrow (((x \gt y) \wedge (x = x)) \vee ((x \leq y) \wedge (x = y)))$, we observe that if we have $(x \gt y)$ then $((x \gt y) \wedge (x = x))$ is true, since $x = x$ is always true. Then we obviously have the entire disjunction.
Similarly, for $\emptyset \vdash (x \leq y) \rightarrow (((x \gt y) \wedge (y = x)) \vee ((x \leq y) \wedge (y = y)))$, we observe that if we have $(x \leq y)$ then $((x \leq y) \wedge (y = y))$ is true, since $y = y$ is always true. Then we obviously have the entire disjunction.
Example 20.4. The following is a proof of a program for $y = |x|$.
| $\llparenthesis \texttt{T} \rrparenthesis$ | |||||||||||||||||
if (x > 0) { | |||||||||||||||||
| $\quad \llparenthesis x \gt 0 \rrparenthesis$ | if-then-else | ||||||||||||||||
| $\quad \llparenthesis x \geq 0 \rrparenthesis$ | implied | ||||||||||||||||
$\quad$ y = x; |
This example was pretty straightforward, but if we wanted to derive a stronger precondition, we could do it by putting together the conditions we already know and pushing them up. For instance, we can get $((x > 0) \rightarrow (x \geq 0)) \wedge ((\neg (x > 0)) \rightarrow (-x \geq 0))$ and it would be a matter of showing $$\emptyset \vdash ((x > 0) \rightarrow (x \geq 0)) \wedge ((\neg (x > 0)) \rightarrow (-x \geq 0)).$$