what is a loop invariant ?

Question

I'm reading "Introduction to Algorithm" CLRS. and the authors are talking about loop invariants, in chapter 2 (Insertion Sort). I don't have any idea of what it means.

Answer 1

Invariant in this case means a condition that must be true at a certain point in every loop iteration.

In contract programming, an invariant is a condition that must be true (by contract) before and after any public method is called.

Answer 2

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:

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 termination condition!) or that j <= 9 && j >= 0.

Answer 3

I like this very simple definition:

A loop invariant is a condition [among program variables] that is necessarily true immediately before and immediately after each iteration of a loop. (Note that this says nothing about its truth or falsity part way through an iteration.)

Source: http://www.cs.uofs.edu/~mccloske/courses/cmps144/invariants_lec.html

By itself, a loop invariant doesn't do much. However, given an appropriate invariant, it can be used to help prove the correctness of an algorithm. The simple example in CLRS probably has to do with sorting. For example, let your loop invariant be something like, at the start of the loop, the first i entries of this array are sorted. If you can prove that this is indeed a loop invariant (i.e. that it holds before and after every loop iteration), you can use this to prove the correctness of a sorting algorithm: at the termination of the loop, the loop invariant is still satisfied, and the counter i is the length of the array. Therefore, the first i entries are sorted means the entire array is sorted.

An even simpler example is shown at http://academic.evergreen.edu/curricular/dsa01/loops.html.

The way I understand a loop invariant is as a systematic, formal tool to reason about programs. We make a single statement that we focus on proving true, and we call it the loop invariant. This organizes our logic. While we can just as well argue informally about the correctness of some algorithm, using a loop invariant forces us to think very carefully and ensures our reasoning is airtight.

Answer 4

In the simplest terms, it's something that will not change at any point in a given loop. They're useful because, since they don't change within the loop they can often be moved outside the loop to reduce the computation done each loop, thus improving execution speed. It's a pretty common optimisation technique used by most compilers.

A very contrived example:

for (int i = 0; i < 10; i++)
{
    ...
    int value = 1 + 2 + 3 + 4;
    ...
    doSomething (value, i);
    ...
}

optimised to:

int value = 1 + 2 + 3 + 4;
for (int i = 0; i < 10; i++)
{
    ...
    doSomething (value, i);
    ...
}

saving computation of value each time through the loop.