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.
By induction on i we can prove the following equality
provided . Thus, can be chosen as the weakest precondition of with respect to .
C = while Y2n do
Determine provided the values of X and Y are integers.
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,