How am I supposed to show the predicate as true?

Question

Given a while loop and a predicate. Show that if the predicate is true before entry to the loop, then it is also true after exit from the loop.

predicate: m^3 > n^2 while (m ≥ 0 and m ≤ 100) do

m := 3 · m

n := 5 · n

end while

I tried to plug the m and n values into the predicate, but just got 27m^3>25n^2.

Answer 1

Proof:

m^3 > n^2 >=0 is given. It must be greater than or equal to zero because when you

square a number, the result is positive or zero.

So m is positive since m^3 > 0, because the cube root of a positive cube is positive.

Assuming the condition of the while loop tests TRUE,

m := 3*m and N := 5 * n,

so (3m)^3 = 27*m^3

> 27 n^2 <---- since m^3 > n^2

> 25*n^2 <--- since 27 > 25

= (5n)^2

so that is the proof thant (2m)^3 > (5n)^2 upon exit of the loop.

However it is possible that the loop MAY NOT execute.

for n=-1000, n^2 = 1000000. since M^3 is greater than that,

that forces M to be greater than 100, in which case the loop

will not execute