Loop Invariant Integer Division

Integer Division

This is the 5th part in a series of short articles on loop invariants. You can refer to the first part (introduction) here. Our example for today is a little bit harder than the previous examples. We are going to develop an algorithm to do integer division. Let us see how can we use loop invariants to develop a correct integer division algorithm.

Problem definition

Given two positive integers (n) and (q) find the integer division (n/q) for example if (n = 9) and (q = 2) then (n/q = 4)

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

The goal of the algorithm is to split the value of (n) into (d) smaller values each of which is (q) and some remainder (r). In other words we need to find (d) and (r) such that the following expression is true (n = q * d + r and r < d) where (d) is the integer division and (r) is the remainder. Note that (r) must be less than (d) otherwise we can just subtract one more (d) from (n) and add one to the final result. Here is an example, when (n = 9) and (q = 2) then we have (d = 4) and (r = 1)

so the post condition should be as follows:

Write the loop specifying the guard (loop condition)

As we used to do before, 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:

The reason why we chose (r >= d) as the loop guard is because it is the negation of the post condition (r < d). The only way to exist the loop is when (r >= d) is false which means (r < d) indicated by the post condition. 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. The loop invariant we choose is (n = q * d + r). Note that (q) keeps how many times we can subtract a (d) from (n) until no longer we can do so.

Fix the initialization so that the loop invariant evaluate to true

Recall that (q) represents the number of times we can subtract a (d) from (n) until we can no longer do that. If we start at (q = 0) then (r) has to be initialized to (n) in order for the invariant (n = q * d + r) to hold true just before entering the loop

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

As we mentioned earlier we should keep subtracting a (d) from (n) until we can no longer do that when the loop condition is false. So we need two statements to achieve that. The first one is (r = r – d) and the reason why it is not (n = n – d) is because we already initialized (r = n). The other statement that we need is (q = q + 1) simply because whenever we subtract a (d) from (n) we count it in (q). let us see if these two statements keep the invariant true as the loop progresses. In the first iteration we will have (r = r – d = n – d) and (q = q + 1 = 0 + 1 = 1). Substitute these values in the invariant:

So far we proved that the invariant is true at initialization stage and after each iteration. Now let us prove it is true after the loop terminates. When the loop terminates it should have executed (q + 1) times and therefore we should have subtracted a (d) from (n) also (q + 1) times. At that time (r) will be equal to (n – (q + 1) * d). Now substitute these values and see how the invariant holds true after the loop exists:

Here is how the final code looks like:

We are done for toady. In the next article we will discuss a new example “Linear Search“. Thanks for reading.