wp( if x then x := x else x := 0 – x fi, x ≤ 0 ). (25%)
wp that wp(C, not Q) → not wp(C, Q) for any language construct C and any assertion Q. (25%)
{ n > 0 }
i := n;
fact := 1;
while i do
fact := fact * i;
i := i – 1
od
{ fact = 1 * 2 * … * n }