Loop Invariant Array Sum

Array sum

Hello! This is the second 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 sum of all elements in an array. It is very easy to solve this problem using intuition but the purpose here is to learn more about loop invariants. Let us get started.

Problem definition

Given an array (A) of (n) integers, calculate the sum of all elements in the array. Identify a loop invariant and show that it holds true before the loop and after each iteration of the loop. Assume the array index starts at (1).

Identifying loop invariant

With more practice, we should become experienced enough to identify loop invariants quickly however, for the sake of demonstration, we will follow the same steps we outlined in the first part (introduction) as follows:

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

The goal of the loop should be something like “Some variable (S) holds the sum of all elements in the array”

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:

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. A good loop invariant would be “The variable (S) holds the sum of the first (k) elements”. In other words: S = A[1] + … + A[k]

Fix the initialization so that the loop invariant evaluate to true

Let us initialize the sum variable (S) with a zero value. In this case, the value of (k) in the invariant expression S = A[1] + … + A[k] should be initialized to zero as well, other wise we will not get a zero sum. For example if (k = 1) then the sum will be just A[1] which is not consistent with (S = 0).

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

The final step is fill the loop body with the required logic to solve the problem. In our case we are accumulating array values into the (S) variable. All we need is a statement like S = S + A[k] which is directly deduced from the loop invariant that we selected. Note that we should put the statement S = S + A[k] right after we increment the loop index (k) simply because we already set (k = 0) in the initialization stage.

Another loop invariant

The loop invariant that we selected previously required us to initialize (k = 0 and S = 0). We also had to choose (k < n) as the loop guard. What if we choose the following loop invariant:

In order for the loop invariant to hold true before entering the loop we should initialize (k = 1) and here is why:

In order for the loop invariant to hold true at the end of the while loop we should put the statement S = S + A[k] before we increment the loop index (k). We can verify that using the first iteration. When (k = 1) the statement S = S + A[k] becomes S = 0 + A[1] = A[1] then (k) becomes (2) after it gets incremented so the invariant becomes

Finally the loop guard has to be (k <= n) instead of just (k < n) so that the post condition holds true once the while loop terminates. Let us assume the array has (10) elements so if we keep the guard as (k < n) then the loop terminates when (k = 10) but in this case the post condition will be:

In summary, initialization stage, filling the body of the loop and choosing a loop guard all have to be consistent with the loop invariant we choose. If they are not then the invariant might not hold true which will probably lead to incorrect code. That is it for today, in the next article we will discuss the "Power” example. Thanks for reading.