Solution.First of all, we apply Lemmas 52 and 53 for finding the formula requested. In addition, in what follows we also take into account the following straightforward properties of the wp-calculus.

With this in hand, we can expand by Lemmas 52 and 53:

By induction on

iwe can prove the following equality

provided . Thus, can be chosen as the weakest precondition of with respect to .

C = while Y2n do

X:=X+Y;

Y:=Y+2

od

Determine provided the values of

XandYare integers.

Solution.

By induction on

iwe can prove that, if , then

Observe, that, if , then

Ybecomes negative, but the relations withYandXstill hold. Hence,