Question

Use a loop invariant to prove that the following program segment for computing the nth power, where n is a positive integer, of a real number x is correct.

power := 1
i := 1
while i <= n
  power := power*x
  i := i+1

Answer 1

Let p be the loop invariant and we need to prove that before, inside and termination of loop “power = x i−1 and i ≤ n + 1.”.

For iniatial case: i=1 and power = x^i-1 = x⁰ =1;

In the loop: i<=n; Since I is incerement by 1; and we know that power_initial =x^i-1;

So, the new power will be power_new= power_initial*x= x^i-1*x = x^i-1+1 = x^(i+1)-1 ;

Now, We know that i=i+1; for new case

Then, on putting i in the place of (i+1), for new case

We get power_new= x^i-1 ;

This process goes throughout the loop.

Now, after the termination of loop, ie. i<=n is false;

We get i=n+1;

by putting the value of i in power

power_n = x^i-1 = x^n+1-1 = xⁿ.

I hope it helps.
Thank you