Proving a code fragment correct under partial correctness 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\}$$
 A: 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?
A: 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.
