Leveraging the Power of Loops with Loop Invariants.

Have you gotten into a situation where it was hard to keep track of what is wrong with your loop because the loop either runs forever without terminating or it gives results that were not expected? One way to leverage on your loops and show that your loops correctly give the desired result is to prove your loops with loop invariants.

 

What is a loop invariant

A loop invariant is a proof technique that is used to show that the algorithm for a loop is correct. Many people think that it is a very hard concept because it is usually expressed in mathematical terms, but they never know that it is not only simple, but it gives you power with your loops. To derive a loop invariant, you should already have the algorithm for the loop and because this is the case, loop invariant proofs are intuitive ways of proving that an algorithm is correct because the programmer already has a base to start from.

A loop invariant starts with a statement about a loop. Let’s call that statement about the loop, L. In the loop invariant we would prove the following things about L:

a. L is true before the loop is entered.

b. For each iteration of the loop, L is true at the end of any iteration.

c. When the loop exits, the statement L, should also be true.

Then, at the exit of the loop or when it terminates, we should have reached our goal when formulating L.

Now let’s illustrate the properties above visually to show how it relates to an example loop:

    
# the Loop Invariant, L, must be true here
while ( TEST CONDITION ):
    # top of the loop
      ...
    # bottom of the loop
    # the Loop Invariant,L, must be true here
# Termination + Loop Invariant = Goal

Now sometimes people confuse what we call the loop invariant with the test condition that terminates the loop. They are two different entities and should not be exchanged one for the other.

Now that we have the properties for a loop invariant, let us illustrate this with an example code on how we can use a loop invariant to justify the correctness of an algorithm.

For example, given the function below, smallest, which is used to find the smallest index at which the target, value, occurs in the sequence, S.

    
def smallest(S, value):
    ''' returns the smallest index at which 
    value is found in sequence, S '''
    n = len(S)
    j = 0  # loop invariant true
    while j < n:
        if S[j] == value:
            return j  # match found at index j
        j += 1  # loop invariant true
    return -1  #loop invariant true

Now look at the algorithm and ask yourself: What can be true before the loop, can be true at the end of each iteration in the loop, and can also be true when the loop terminates (when j >= n)? I labelled the loop invariants as comments to help you. You can see that before the start of the loop, we have not found the smallest index for value. If each iteration in the loop ends, that means we have not still found the smallest index for value. And if the loop eventually terminates and returns -1, we still have not found the smallest index for value. Therefore, the loop invariant here is, L: the smallest index for value has not been found.

So, at loop termination, where j >= n, we have reached our goal which is to prove that there is no smallest index for value in S. But if there is, we have also reached another goal which is to show that the smallest index, j, for value exists. It also helps us to walk through the logic of the loop to show that in whatever of the outcomes happens, we will reach our goal.

Why would this prove that the algorithm is correct? Because in all these instances where the loop invariant is true, it promises us that the loop will terminate successfully and never go into an endless loop and also that it will return the expected index for value, j, if there is value in the sequence, S.

I believe you have gotten the drift of loop invariants and how they help in proving loop algorithms.

Let’s do one more example, this time using a for loop. In the code below, we want to prove that the function, sum_values, will always return the sum of the items in the sequence, S, provided the items are ints.

    
def sum_values(S):
    ''' returns the sum of the items in S
    where items are ints '''
    total = 0 # loop invariant true
    for item in S:
        total += item  # loop invariant true
    return total # loop invariant true

Now, what would be the loop invariant? Look carefully at the code. You will see that before the loops is entered, we declared a variable total and assigned it the value 0. Now, total is supposed to give us the total sum of the items in S. So, before the loop is entered, total gave 0, which is the total sum if we had not accessed the loop. This is true. Now when we entered the loop, at the end of each iteration of the variable item, total will give us the sum of all the items to that point. This is also true at the end of each iteratioin. So, the loop invariant that total gives the total sum is true. When the loop exits, that is, when the items in S are finished, total will return giving us the total sum of the items in S. This is also true for the loop invariant. So, we have proved that our algorithm is correct. Total which the function returns will always give us the total sum of the items in the sequence, S.

Interesting, not so? Yes, and very good way to prove your loops. I tell you, I never have loops that give false results or run into an infinite loop since I discovered loop invariants. That is why I thought it was pertinent to share it with you. It would be selfish for me not to.

I hope you enjoyed this post and would like to use loop invariants to prove your algorithms. You will surely enjoy doing so. If you would like to receive regular updates from my blog, just subscribe by email. Hope to see you soonest.

Happy pythoning.