Loop invariant to prove correctness

“Loop invariant is a invariant defined part of tuple mathematics. It is used to prove the correctness of a loop. The below is the formula,

Metaphor

   So, you got the formula directly fetched from Wikipedia!! Did you understand it? :) The funny part this is logical mathematics which doesn’t have a metaphor or beauty to compare with.

  This technique is like theorem proving, where you consider something is true through out. Only if it is true, the theorem is also true. There are many popular theoretical way to prove a theorem,

   - proof by induction

   - proof by contradiction

There are many more theorem proving techniques available. But logical way to prove a computer program is: Hoare logic which is the formula given above

here, I is the loop invariant, C is the condition for loop termination, if you see the formula, I is maintained initial and in body and also in termination.

Concept

   Why do you want to prove correctness of a computer program? An algorithm can always fail!! There are boundary conditions, negative inputs, infinite loops and all such possibilities when you write a code which is never covered in an algorithm. How would you know that an algorithm never gives infinite loop? the simple way is loop invariants.

   In all the algorithms discussed till now, we should have used loop invariant to confirm the correctness of the code. But since this concept is little bit complex, we have covered a separate section for this. This is really important if you want to write a valid unit test for any code.

  How would you find a loop invariant??

Read fully the below link: http://www.cs.cmu.edu/afs/cs.cmu.edu/academic/class/15211/fall.97/www/lectures/lect0916

The various steps in which loop invariant should be maintained are:

1. Initialization (Assume some loop invariant), Before loop start

2. Execution (Revise the loop invariant so that its true even with the initial assumption), Loop running

3. Termination (The initial assumption should be maintained or revised loop invariant should hold), Loop ended

After analysing all the above algorithm steps, we should come with a single loop invariant which is true.

Examples

• Insertion sort
• loop invariant is for A[0..j-1], A[0] <= A[1] <=… <=A[j-1] where j-1 is the end of the sorted list.
• Linear search
• loop invariant which will be always true is: key is no found in A[j], where j is some index until which we have not found the key yet!!. If j>=n, then we already passed the size of A and hence key is not found.
• Binary search
• end is the last index, start is the first index of an array A, key is the value to search for.
• loop invariant is: A[j]  < key for all j –> end, where j is the mid index at any iteration OR A[j] > key for all start –> j, where j is the mid index at any iteration

Important points

• Loop invariants is very useful for proving the correctness of a program. Can be used for recursive as well as loop based algorithms
• Invariants are basically nothing but ASSERTs in our code. It just verifies the precondition for a function. But Loop invariants can be used to test both pre and post conditions and successful return of the value. Used for doing unit testing.
• Understanding the loop invariant of an algorithm catches bugs in code!!!.. THIS IS THE MOST IMPORTANT USE OF LOOP INVARIANT