The wp-calculus

Exercise 25. Let

C = while X0 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 Y2n 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, .