Vfrdtyky

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.

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.

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.

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.

It should be noted that a Loop Invariant can help in the design of iterative algorithms when considered an assertion that expresses important relationships among the variables that must be true at the start of every iteration and when the loop terminates. If this holds, the computation is on the road to effectiveness. If false, then the algorithm has failed.

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.

The meaning of invariant is never change

Here the loop invariant means "The change which happen to variable in the loop(increment or decrement) is not changing the loop condition i.e the condition is satisfying " so that the loop invariant concept has came

It is hard to keep track of what is happening with loops. Loops which don't terminate or terminate without achieving their goal behavior is a common problem in computer programming. Loop invariants help. A loop invariant is a formal statement about the relationship between variables in your program which holds true just before the loop is ever run (establishing the invariant) and is true again at the bottom of the loop, each time through the loop (maintaining the invariant).
Here is the general pattern of the use of Loop Invariants in your code:

...
// the Loop Invariant must be true here

while ( TEST CONDITION ) {

// top of the loop

...

// bottom of the loop

// the Loop Invariant must be true here

}

// Termination + Loop Invariant = Goal

...

Between the top and bottom of the loop, headway is presumably being made towards reaching the loop's goal. This might disturb (make false) the invariant. The point of Loop Invariants is the promise that the invariant will be restored before repeating the loop body each time.
There are two advantages to this:

Work is not carried forward to the next pass in complicated, data dependent ways. Each pass through the loop in independent of all others, with the invariant serving to bind the passes together into a working whole.
Reasoning that your loop works is reduced to reasoning that the loop invariant is restored with each pass through the loop. This breaks the complicated overall behavior of the loop into small simple steps, each which can be considered separately.
The test condition of the loop is not part of the invariant. It is what makes the loop terminate. You consider separately two things: why the loop should ever terminate, and why the loop achieves its goal when it terminates. The loop will terminate if each time through the loop you move closer to satisfying the termination condition. It is often easy to assure this: e.g. stepping a counter variable by one until it reaches a fixed upper limit. Sometimes the reasoning behind termination is more difficult.

The loop invariant should be created so that when the condition of termination is attained, and the invariant is true, then the goal is reached:

invariant + termination => goal

It takes practice to create invariants which are simple and relate which capture all of goal attainment except for termination. It is best to use mathematical symbols to express loop invariants, but when this leads to over-complicated situations, we rely on clear prose and common-sense.

Sorry I don't have comment permission.

@Tomas Petricek as you mentioned

A weaker invariant that is also true is that i >= 0 && i < 10 (because this is the continuation condition!)"

How it's a loop invariant?

I hope I am not wrong, as far as I understand^[1], Loop invariant will be true at the beginning of the loop (Initialization), it will be true before and after each iteration (Maintenance) and it will also be true after the termination of the loop (Termination). But after the last iteration i becomes 10. So, the condition i >= 0 && i < 10 becomes false and terminates the loop. It violates the third property (Termination) of loop invariant.

[1] http://www.win.tue.nl/~kbuchin/teaching/JBP030/notebooks/loop-invariants.html

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.

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.

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

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

In Linear Search (as per exercise given in book), we need to find value V in given array.

Its simple as scanning the array from 0 <= k < length and comparing each element. If V found, or if scanning reaches length of array, just terminate the loop.

As per my understanding in above problem-

Loop Invariants(Initialization):
V is not found in k - 1 iteration. Very first iteration, this would be -1 hence we can say V not found at position -1

Maintainance:
In next iteration,V not found in k-1 holds true

Terminatation:
If V found in k position or k reaches the length of the array, terminate the loop.