## The wp-calculus

Exercise 25. Let

C = while X 0 do

X:=X+1;

Y:=Y-2

od

Determine the value of .

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 i we can prove the following equality provided . Thus, can be chosen as the weakest precondition of with respect to .

Exercise 26. Let

C = while Y 2n do

X:=X+Y;

Y:=Y+2

od

Determine provided the values of X and Y are integers.

Solution. By induction on i we can prove that, if , then Observe, that, if , then Y becomes negative, but the relations with Y and X still hold. Hence, Exercise 27. Let

C = while Y do

Z:=f(Y)Z;

Y:=t(Y)

od

Determine .

Solution. In general, we obtain provided . Thus, .

Exercise 28. Let

C = while Y do

Z:=Zf(Y)f(Y);

Y:=t(Y)

od

Determine .

Solution. Let denote the word , if . Then By induction on i we obtain Thus, .