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

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.

Answer 2

I like this very simple definition: (source)

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.)

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: Loops Invariants, Correctness, and Program Derivation.

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.