Proof of Loop Invariant and Algorithm

Question

How would I get a loop invariant and prove it for the following algorithm.

power(x,y):
   z = 1
   m = 0
   while m < y:
       z = z*x
       m = m+1
   return z

Answer 1

Firstly, I think you mean z = z*x To show the loop invariant for any given loop, you have to come up with a statement that doesn't change at the beginning and end of any iteration. Using that invariant, you will prove that when the program terminates, the function works. your function power is basically trying to do x^y.

Lets construct a loop invariant: Z = x^m. You can see that this is true both at the beginning and end of the loop.

You also know that loop can only exit when not(m= y, or m =y.

So if Z=x^m, and upon termination m = y. Then Z = x^y.

So we can see that this program is partially correct.