Proving a code fragment correct under partial correctness

Question

I'm asked to prove the correctness of the following annotated program:

$\{ \text{true} \}$

if (x < y)      m = x - y;
else if (x = y) m = x + y;
else            m = x * y;

$\{ ((x<y) \land m=x-y) \lor ((x=y)\land m=x+y) \lor ((x>y)\land m=x*y) \}$

using the if-else inference rule.

The problem is, I don't really get what that inference rule says. Or in other words, I get the inference rule but it seems to be useless:

$$\{P\land B\}C_1\{Q\},\{P\land \lnot B\}C_2\{Q\}$$

---

$$\{P\} \text{ if}(B) C_1 \text{ else }C_2 \{Q\}$$

Answer 1

Introduction:

Rule $$ \frac{ \{P\land B\}\ C\ \{Q\},\quad\{P\land \lnot B\}\ D\ \{Q\} }{ \{P\}\ \mathtt{if(}B\mathtt{)}\ C\ \mathtt{else}\ D\ \{Q\} } \tag{$\spadesuit$}$$

tells us that given that $\{P\land B\}\ C\ \{Q\}$ and $\{P\land \lnot B\}\ D\ \{Q\}$ are true, we can conclude that $\{P\}\ \mathtt{if(}B\mathtt{)}\ C\ \mathtt{else}\ D\ \{Q\}$ is true.

Example:

Consider the following code:

 {true}
 if (x < 0) y = -x;
 else y = x;
 {y = |x|}

If we want to prove it, we need to fit it into {P} if(B) C else D {Q} rule (because it is the only one that contains if), so we know that {P} = {true}, {B} = {x < 0}, and {Q} = {y = |x|}. To use $(\spadesuit)$ we should first make sure that {P ∧ B } C {Q} and {P ∧ ¬B} D {Q} hold. However, {x < 0} y = -x {y = |x|} and {x ≥ 0} y = x {y = |x|} are both true by the rule of assignment (and some simplification), hence, the premise of $(\spadesuit)$ is satisfied and we can conclude that our code is correct.

Can you extend this example to your code?

Answer 2

Apparently, the $P$ we need is "true", the $Q$ we need is the long statement at the end of the code, the condition $B$ is $x<y$, statement $C_1$ is m= x - y and $C_2$ is itself an if-then construct, namely if (x = y) m = x + y; else m = x * y;. So to apply the inference rule you need the two premises as mentioned. The first is just $$ \{\text{true}\land x<y\}\text{m = x - y}\{ ((x<y) \land m=x-y) \lor ((x=y)\land m=x+y) \lor ((x>y)\land m=x*y) \}$$ and should not be hard. For the second, you need to deal with the remeining if-then in a similar way.