Loop Invariant Factorial

Factorial

Hello everyone! This is the 4th part in a series of short articles on loop invariants. You can refer to the first part (introduction) here. We are going to continue talking about loop invariants. Let us see how to find an appropriate loop invariant to calculate the factorial of a positive integer.

Problem definition

Given a positive integer (n), develop an algorithm to calculate the factorial of (n). Identify a loop invariant to prove the correctness of your algorithm.

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

The goal of the loop should be something like “Result = product of all numbers between (1) and (n)”. This is indeed the definition of factorial for example the factorial of (5) is (1 x 2 x 3 x 4 x 5)

Write the loop specifying the guard (loop condition)

Again, 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:

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) = product of all numbers between (1) and (k)”

Fix the initialization so that the loop invariant evaluate to true

When (n = 1) no multiplication is needed and the result evaluates to (1) so let us initialize the result as (R = 1). This requires us to initialize (k = 1). With (R = 1 and k = 1) the invariant holds true before entering the loop because we need to multiply the numbers between (1) and (1) which is only (1) sound silly ha!

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

We need to calculate the product of all numbers between (1) and (k). In order to do that we can use a statement like (R = R * k). As you can see the statement (R = R * k) depends on the loop index (k) so it is very important to determine where to put it (before or after we increment the loop index (k)). The right place for it is after we increment the loop index (k). The reason why it should be after we increment the loop index (k) is because it makes the loop invariant hold true after each iteration and most importantly after the loop exits when (k = n). For example if we put it before we increment the loop index (k) the loop invariant keeps true until we exit the loop, at that point the last number (n) is not included in the product which is wrong. Note also that we can put (R = R * k) before we increment the loop index (k) only if we change the load guard from (k < n) to (k <= n).

Note that the loop terminates when (k = n). At that time the loop invariant evaluates to

That is exactly the goal of the algorithm or the post condition mentioned in step 1. That is it for today, in the next article we will discuss a new example "Integer Division“. Thanks for reading.

Add a Comment

Your email address will not be published. Required fields are marked *