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, it is a LOOP condition that is true in every loop iteration:

for(int i=0; i<10; i++)
{ }

In this we can say state of i is i<10 and i>=0

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.

Answer 3

Previous answers have defined a Loop Invariant in a very good way.

Now let me try to explain how authors of CLRS used Loop Invariants 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 (Source: CLRS book): Subarray[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 Subarray [1:1] is the array to be tested.As it has only one element so it is sorted.Thus Invariant is satisfied.

Maintanence: 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 algorithm.

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

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

Answer 4

A loop invariant is an assertion that is true before and after loop execution.

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

Answer 6

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.