Concepts of Programming Languages

156 Chapter 3 Describing Syntax and Semantics

For zero iterations, the weakest precondition is, obviously,

{y = x}

For one iteration, it is

wp(y = y + 1, {y = x}) = {y + 1 = x}, or {y = x - 1}

For two iterations, it is

wp(y = y + 1, {y = x - 1})={y + 1 = x - 1}, or {y = x - 2}

For three iterations, it is

wp(y = y + 1, {y = x - 2})={y + 1 = x - 2}, or {y = x – 3}

It is now obvious that {y < x} will suffice for cases of one or more iterations.

Combining this with {y = x} for the zero iterations case, we get {y <= x},

which can be used for the loop invariant. A precondition for the while state-

ment can be determined from the loop invariant. In fact, I can be used as the

precondition, P.

We must ensure that our choice satisfies the four criteria for I for our

example loop. First, because P = I, P => I. The second requirement is that it

must be true that

{I and B} S {I}

In our example, we have

{y <= x and y <> x} y = y + 1 {y <= x}

Applying the assignment axiom to

y = y + 1 {y <= x}

we get {y + 1 <= x}, which is equivalent to {y < x}, which is implied by

{y <= x and y <> x}. So, the earlier statement is proven.

Next, we must have

{I and (not B)} => Q

In our example, we have

{(y <= x) and not (y <> x)} => {y = x}

{(y <= x) and (y = x)} => {y = x}

{y = x} => {y = x}

So, this is obviously true. Next, loop termination must be considered. In this

example, the question is whether the loop

{y <= x} while y <> x do y = y + 1 end {y = x}