Weakest precondition for selection

Hej,

Jeg skal beregne weakest precondition for følgende selection-programkode:

{P: x≥0 ∧ y≥0 ∧ z≥0 }
if (x > y && x > z)
max = x;
else if (y > x && y > z)
max = y;
else
max = z;
{Q: max≥x ∧ max≥y ∧ max≥z ∧ ( max=x ∨ max=y ∨ max=z )}

Indtil videre er jeg kommet frem til:

wp(A,Q)≡wp(if B then S1 else S2)≡
(B∧wp(S1,Q))  v (¬B ∧wp(S2,Q))≡
(B∧wp(S1,Q))v(¬B ∧(if S2.B then S2.S1 else S2.S2,Q))
(B ∧wp(S1,Q))v (¬B ∧((S2.B∧wp(S2.S1,Q)) v (¬S2.B ∧wp (S2.S2,Q))) =
(B ∧wp(S1,Q))v (¬B ∧S2.B∧wp(S2.S1,Q)) v (¬B ∧ ¬S2.B ∧wp (S2.S2,Q))

Der er indsat bogstaver i den nederste linie for at gøre det mere overskueligt:
B: (x > y && x > z)
S1: max = x
S2.B: y > x && y > z
S2.S1: max = y
S2.S2: max = z

Er der nogen der ved hvordan man så kommer videre?

Tak!