What is a loop invariant?

Question

I'm reading "Introduction to Algorithm" by CLRS. In chapter 2, the authors mention "loop invariants". What is a loop invariant?

Answer 1

The Loop Invariant Property is a condition that holds for every step of a loops execution (ie. for loops, while loops, etc.)

This is essential to a Loop Invariant Proof, where one is able to show that an algorithm executes correctly if at every step of its execution this loop invariant property holds.

For an algorithm to be correct, the Loop Invariant must hold at:

Initialization (the beginning)

Maintenance (each step after)

Termination (when it's finished)

This is used to evaluate a bunch of things, but the best example is greedy algorithms for weighted graph traversal. For a greedy algorithm to yield an optimal solution (a path across the graph), it must reach connect all nodes in the lowest weight path possible.

Thus, the loop invariant property is that the path taken has the least weight. At the beginning we haven't added any edges, so this property is true (it isn't false, in this case). At each step, we follow the lowest weight edge (the greedy step), so again we're taking the lowest weight path. At the end, we have found the lowest weighted path, so our property is also true.

If an algorithm doesn't do this, we can prove that it isn't optimal.

Answer 2

Loop invariant is a mathematical formula such as (x=y+1). In that example, x and y represent two variables in a loop. Considering the changing behavior of those variables throughout the execution of the code, it is almost impossible to test all possible to x and y values and see if they produce any bug. Lets say x is an integer. Integer can hold 32 bit space in the memory. If that number exceeds, buffer overflow occurs. So we need to be sure that throughout the execution of the code, it never exceeds that space. for that, we need to understand a general formula that shows the relationship between variables. After all, we just try to understand the behavior of the program.

Answer 3

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.