#### [SOLVED] What is a loop invariant?

By Attilah

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

#### 15 comments #### @Tushar Kathuria 2015-01-05 07:12:22

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. #### @Gaurav Aradhye 2015-08-29 21:43:21

Agree... termination statement is so important here. #### @timkofu 2018-10-10 13:54:15

A loop invariant is an assertion that is true before and after loop execution. #### @Tomas Petricek 2010-07-11 02:10:59

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`. #### @Brian S 2010-07-11 02:17:53

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 2011-04-07 16:23:54

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 2011-10-19 09:52:38

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 2012-04-07 22:47:02

@Tomas Petricek - when the loop terminates, i = 10 and j = -1; so the weaker invariant example you gave may not be correct (?) #### @Nishant Kumar 2012-11-06 13:22:23

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) #### @Flavius 2013-01-03 20:21:31

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. #### @bright-star 2013-11-28 02:56:47

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 2014-03-24 20:49:41

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 2014-06-09 00:12:06

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). #### @Brian Yeh 2015-09-08 08:24:21

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. #### @jburns20 2018-02-27 21:36:49

@Raja Updated the answer to take this problem into account, and also conform more closely to the formulation in CLRS. #### @TNi 2010-07-11 02:17:07

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. #### @Robert S. Barnes 2013-03-12 09:28:09

It should be pointed out that "immediately after each iteration" includes after the loop terminates - regardless of how it terminated. #### @Neekey 2018-12-05 12:33:09

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! #### @i.maddy 2017-10-28 13:59:53

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` #### @Alex Mapley 2017-03-09 01:13:50

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. #### @Mahmudul Haque 2016-11-05 05:10:33

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, 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. #### @muiiu 2017-07-24 04:44:14

My guess is that this is true because the loop doesn't actually execute under those conditions. #### @Tilak raj 2015-09-09 19:07:00

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. #### @AndroDev 2015-08-27 08:49:43

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. #### @Mehmet YILMAZ 2015-05-30 20:11:55

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. #### @sasidhar 2014-09-19 07:02:34

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 #### @Robert S. Barnes 2013-03-12 08:48:56

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. #### @acgtyrant 2019-01-24 00:27:29

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. #### @Vahid Rafiei 2012-12-02 17:38:58

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. #### @kdazzle 2012-12-12 22:29:53

Formal finger proof? #### @Vahid Rafiei 2012-12-14 01:11:42

It's just an example, not a proof. If I understood you correctly.. #### @kiwicomb123 2018-03-25 23:20:54

Jeff was a prof at my school! #### @Eric Steen 2011-09-28 02:09:32

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. #### @Mark Rushakoff 2010-07-11 02:10:26

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.

### [SOLVED] What exactly is RESTful programming?

• 2009-03-22 14:45:39
• hasen
• 1599657 View
• 3839 Score
• 32 Answer
• Tags:   http rest definition