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

User · Answer

In simple words  it is a LOOP condition that is true in every loop iteration   for int i 0  i lt 10  i          In this we can say state of i is i lt 10 and i gt  0

User · Answer

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

User · Answer

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

User · Answer

Sorry I don t have comment permission    Tomas Petricek as you mentioned     A weaker invariant that is also true is that  i    0  amp  amp  i  lt  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  amp  amp  i  lt  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

User · Answer

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  lt   k  lt  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

User · Answer

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

User · Answer

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

User · Answer

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

User · Answer

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    before the loop starts before each iteration of the loop 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  lt   end             mid   floor start   end   2           if   A mid     a   return mid         if   A mid   gt  a   end   mid - 1         if   A mid   lt  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  lt   mid  lt   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  gt  end then there can be no number such that start  lt   mid and mid  lt   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  amp  amp  start  lt   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

User · Answer

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  gt  0 and A i   gt  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

User · Answer

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

User · Answer

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

User · Answer

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 lt 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  gt   0  amp  amp  i  lt   10

User · Answer

Definition by How to Think About Algorithms  by Jeff Edmonds  A loop invariant is an assertion that is placed at the top of a loop and that must hold true every time the computation returns to the top of the loop

User · Answer

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

User · Answer

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

[algorithm] What is a loop invariant?

Examples related to algorithm

Examples related to terminology

Examples related to definition

Examples related to clrs

Examples related to loop-invariant