Question

I had a question about loop invariants. I was hoping someone could explain them and give a few examples so I can see how they work. Thanks.

Answer 1

A loop invariant is a formal statement about the relationship between variables in your program which holds true just before the loop is ever run (establishing the invariant) and is true again at the bottom of the loop, each time through the loop (maintaining the invariant).

Here is the general pattern of the use of Loop Invariants in your code:

...
// the Loop Invariant must be true here
while ( TEST CONDITION ) {
// top of the loop
...
// bottom of the loop
// the Loop Invariant must be true here
}
// Termination + Loop Invariant = Goal

In simple words, a loop invariant is some predicate (condition) that holds for every iteration of the loop. For example, let's look at a simple for loop that looks like this:

Example 1:

int j = 9;
for(int i=0; i<10; i++)
j--;
In this example it is true (for every iteration) that i + j == 9. A weaker invariant that is also true is that i >= 0 && i < 10 (because this is the continuation condition!) or that j <= 9 && j >= 0.

There is one thing that many people don't realize right away when dealing with loops and invariants. They get confused between the loop invariant, and the loop conditional ( the condition which controls termination of the loop ).

As people point out, the loop invariant must be true

before the loop starts
before each iteration of the loop
after the loop terminates
( although it can temporarily be false during the body of the loop ). On the other hand the loop conditional must be false after the loop terminates, otherwise the loop would never terminate.

Thus the loop invariant and the loop conditional must be different conditions.
Example 2:

A good example of a complex loop invariant is for binary search.

bsearch(type A[], type a) {
start = 1, end = length(A)

while ( start <= end ) {
mid = floor(start + end / 2)

if ( A[mid] == a ) return mid
if ( A[mid] > a ) end = mid - 1
if ( A[mid] < a ) start = mid + 1

}
return -1

}

So the loop conditional seems pretty straight forward - when start > end the loop terminates. But why is the loop correct? What is the loop invariant which proves it's correctness?

The invariant is the logical statement:

if ( A[mid] == a ) then ( start <= mid <= end )
This statement is a logical tautology - it is always true in the context of the specific loop / algorithm we are trying to prove. And it provides useful information about the correctness of the loop after it terminates.

If we return because we found the element in the array then the statement is clearly true, since if A[mid] == a then a is in the array and mid must be between start and end. And if the loop terminates because start > end then there can be no number such that start <= mid and mid <= end and therefore we know that the statement A[mid] == a must be false. However, as a result the overall logical statement is still true in the null sense. ( In logic the statement if ( false ) then ( something ) is always true. )

Now what about what I said about the loop conditional necessarily being false when the loop terminates? It looks like when the element is found in the array then the loop conditional is true when the loop terminates!? It's actually not, because the implied loop conditional is really while ( A[mid] != a && start <= end ) but we shorten the actual test since the first part is implied. This conditional is clearly false after the loop regardless of how the loop terminates.