Loop Invariant Power Function

Power Function

Hello! This is the third part in a series of short articles on loop invariants. You can refer to the first part (introduction) here. In this article we will develop an algorithm to calculate the nth power of a positive integer.

Problem definition

Given two positive integers (x) and (n), develop an algorithm to calculate (x) raised to the power of (n). Identify a loop invariant to prove the correctness of your algorithm. Assume (n > 0).

Identify the goal of the loop and write it as a post condition

The goal of the loop should be something like "Result: (x) multiplied by itself (n) times"

//Post condition: R = x * ... * x
//where the number of * operations = n-1

Write the loop specifying the guard (loop condition)

We will be using a while loop in our demonstration because it clearly separates the guard (loop condition) from initialization and loop index, however we can use any other kind of loop if we wish (for example a for loop). Here is the skeleton of the while loop along with the post condition from step 1:

While (k < n)
{
	k++;
}

//Post condition: R = x * ... * x
//where the number of * operations = n-1

Fill in the loop invariant

Loop invariant should describe the goal of the algorithm. It should hold true just before entering the loop and after each iteration. It should give an idea about the current progress towards the final goal. We suggest a loop invariant like "Result (R) holds the multiplication of (x) by itself (k-1) times"

//Invariant: R = x * ... * x
//where the number of * operations = k-1

While (k < n)
{
	k++;

	//Invariant: R = x * ... * x
	//where the number of * operations = k-1
}

//Post condition: R = x * ... * x
//where the number of * operations = n-1

Fix the initialization so that the loop invariant evaluate to true

When (n = 1) no multiplication is needed and the result evaluates to (x) so let us initialize the result as (R = x). This requires us to initialize (k = 1). With (R = x and k = 1) the invariant holds true before entering the loop because we need k - 1 = 1 - 1 = 0 multiplications.

int R = x;
int k = 1;

//Invariant: R = x * ... * x
//where the number of * operations = k-1

While (k < n)
{
	k++;

	//Invariant: R = x * ... * x
	//where the number of * operations = k-1
}

//Post condition: R = x * ... * x
//where the number of * operations = n-1

Figure out how to achieve the goal by filling in the body of the loop

Raising (x) to the power of (n) is calculated by multiplying (x) by itself (n) times. In order to do that we need a statement like (R = R * x). We can put this statement before or after we increment the loop index (k) because loop invariant is going to hold true in either case. The reason why the invariant holds true in either case is because the statement (R = R * x) does not depend on (k).

int R = x;
int k = 1;

//Invariant: R = x * ... * x
//where the number of * operations = k-1

While (k < n)
{
	R = R * x;

	k++;

	//Invariant: R = x * ... * x
	//where the number of * operations = k-1
}

//Post condition: R = x * ... * x
//where the number of * operations = n-1

Note that the loop terminates when (k = n) so we have k - 1 = n - 1 multiplications by the time we finish the loop. This is exactly the goal of the algorithm (post condition) explained in step 1. That is it for today, in the next article we will discuss a new example "Factorial". Thanks for reading.

One Comment

Leave a Reply