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?

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

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

Solution 3

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

1. before the loop starts
2. before each iteration of the loop
3. 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.

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.

Solution 4

Previous answers have defined a loop invariant in a very good way.

Following is how authors of CLRS used loop invariant to prove correctness of Insertion Sort.

Insertion Sort algorithm(as given in Book):

INSERTION-SORT(A)
    for j ← 2 to length[A]
        do key ← A[j]
        // Insert A[j] into the sorted sequence A[1..j-1].
        i ← j - 1
        while i > 0 and A[i] > key
            do A[i + 1] ← A[i]
            i ← i - 1
        A[i + 1] ← key

Loop Invariant in this case: Sub-array[1 to j-1] is always sorted.

Now let us check this and prove that algorithm is correct.

Initialization: Before the first iteration j=2. So sub-array [1:1] is the array to be tested. As it has only one element so it is sorted. Thus invariant is satisfied.

Maintenance: This can be easily verified by checking the invariant after each iteration. In this case it is satisfied.

Termination: This is the step where we will prove the correctness of the algorithm.

When the loop terminates then value of j=n+1. Again loop invariant is satisfied. This means that Sub-array[1 to n] should be sorted.

This is what we want to do with our algorithm. Thus our algorithm is correct.

Solution 5

Beside all of the good answers, I guess a great example from How to Think About Algorithms, by Jeff Edmonds can illustrate the concept very well:

EXAMPLE 1.2.1 "The Find-Max Two-Finger Algorithm"

1) Specifications: An input instance consists of a list L(1..n) of elements. The output consists of an index i such that L(i) has maximum value. If there are multiple entries with this same value, then any one of them is returned.

2) Basic Steps: You decide on the two-finger method. Your right finger runs down the list.

3) Measure of Progress: The measure of progress is how far along the list your right finger is.

4) The Loop Invariant: The loop invariant states that your left finger points to one of the largest entries encountered so far by your right finger.

5) Main Steps: Each iteration, you move your right finger down one entry in the list. If your right finger is now pointing at an entry that is larger then the left finger’s entry, then move your left finger to be with your right finger.

6) Make Progress: You make progress because your right finger moves one entry.

7) Maintain Loop Invariant: You know that the loop invariant has been maintained as follows. For each step, the new left finger element is Max(old left finger element, new element). By the loop invariant, this is Max(Max(shorter list), new element). Mathe- matically, this is Max(longer list).

8) Establishing the Loop Invariant: You initially establish the loop invariant by point- ing both fingers to the first element.

9) Exit Condition: You are done when your right finger has finished traversing the list.

10) Ending: In the end, we know the problem is solved as follows. By the exit condi- tion, your right finger has encountered all of the entries. By the loop invariant, your left finger points at the maximum of these. Return this entry.

11) Termination and Running Time: The time required is some constant times the length of the list.

12) Special Cases: Check what happens when there are multiple entries with the same value or when n = 0 or n = 1.

13) Coding and Implementation Details: ...

14) Formal Proof: The correctness of the algorithm follows from the above steps.

View more solutions

Comments

[Tom Gullen]

This seems pretty good at explaining: cs.miami.edu/~burt/learning/Math120.1/Notes/LoopInvar.html

[Adil Abbasi]

check this link programmers.stackexchange.com/questions/183815/…

[RBT]

Just in case if someone wants to solve an actual algorithmic coding problem based on the concept of loop invariant then please refer to this problem on HackerRank. They have also referred insertion sort problem only to detail out the concept.

[RBT]

One can also refer the notes here for theoretical understanding.

[Brian S]

This is an excellent example. Many times when I've heard an instructor describe the loop invariant, it has simply been 'the loop condition', or something similar. Your example shows that the invariant can be much more.

[Clash]

I don't see this a good example because the loop invariant should be somewhat the goal of the loop... CLRS uses it to proove the correctness of a sorting algorithm. For insertion sort, supposing the loop is iterating with i, at the end of each loop, the array is ordered until the i-th element.

[Jack]

yeah, this example is not wrong, but just not enough. I back @Clash up, as loop invariant should present the goal, not just for itself.

[Raja]

@Tomas Petricek - when the loop terminates, i = 10 and j = -1; so the weaker invariant example you gave may not be correct (?)

[Nishant Kumar]

Another Simple way : loop invariant - captures what the loop does not do, i.e., what it leaves unchanged over any single execution of the loop body (and hence over the entire execution of the loop)

[Einstein]

Although I agree with the comments above, I've upvoted this answer because ... the goal is not defined here. Define any goal that fits in, and the example is great.

[Robert S. Barnes]

It should be pointed out that "immediately after each iteration" includes after the loop terminates - regardless of how it terminated.

[bright-star]

It's kind of crazy, but a valid loop invariant can be anything that holds at initialization and maintenance steps along the loop, even trivial statements. They're only useful if they reveal the key to the valid progress of the loop.

[trevorkavanaugh]

Just started reading about loop invariants and got confused.. this cleared it up for me. Although simple, it supplements the more complex explanations I have been seeing perfectly. Thanks!

[Filip Vondrášek]

By the way, just for the sake of completion, a loop invariant can also be simply True (it doesn't say anything about the loop, but it always yields true).

[Gaurav Aradhye]

Agree... termination statement is so important here.

[Brian Yeh]

I disagree with the other comments. The fact that this definition did not include the goal of the loop invariant helped me understand it better. Goals are fuzzy and your description provided a concrete answer.

[muiiu]

My guess is that this is true because the loop doesn't actually execute under those conditions.

[jburns20]

@Raja Updated the answer to take this problem into account, and also conform more closely to the formulation in CLRS.

[Neekey]

Thanks very much for this answer! The biggest take from it is the purpose of having this loop invariant is to help prove the correctness of the algorithm. The other answers only focus on what is a loop invariant!

[acgtyrant]

It is stange that to use a logical statement as loop invariant, because as all logical statement can be always true, no matter what condition it is.

[scanny]

Not so strange I should think, since there is no guarantee that a is present in A. Informally it would be, "if the key a is present in the array, it must occur between start and end inclusive". Then it follows that if A[start..end] is empty, that a is not present in A.

[scanny]

I think this answer really "puts its finger" on the intuitive gist of an invariant :).

[Gilbert]

Can we adapt this loop invariant to prove that low - high <= 1?

[kiwicomb123]

Its good to see a York University professor mentioned here. :) The world needs more Jeff Edmonds :)