## Search

### 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