Loop Invariant

Untitled-1

Loop Invariant

As we saw earlier there are two ways to prove the Correctness of an algorithm. But when we look at the practical methods of testing the correctness it is not always possible. Because,

  • Most of the real time programs have a big scale of algorithm
  • For big scale algorithms there are larger types of test data to be tested
  • And the time taken for this analysis is high when the algorithm is big

So most of the time experts stick with the theoretical methods to prove the correctness. Today we are going to see one of those techniques called Loop Invariant.

What is Invariant?

Simply it refers to something that never change.

So when it mentioned as loop invariant, it is a formal statement or assumption about the relation between the variables of the algorithm which never changes for each and every iteration of that particular loop.

For an example, if we assume something as true before the first iteration of the loop it has to be true at the bottom of the loop and also it has to be true for the next iteration as well. It has three main properties

  1. Initialization
  2. Maintenance
  3. Termination

For an algorithm to be correct it has to have the loop invariant for that all three properties have to be satisfied.

 

Loop invariant can be simply explained by the help of the insertion sort algorithm.

loopInitialization: Before us starting to sort the array we assume that the first element (the sorted portion/Sub array/left side of the array) of the array is already sorted. Then we pick the first element from the unsorted portion of the array and check it with the sorted portion and rearrange them if it is necessary.

Maintenance: After the first iteration of the loop now we will have two elements in sorted portion. Now we again assumes that the sorted Captureportion as completely sorted before starting the next iteration. And the assumption is True. Likewise the loop will runs until all the elements are sorted.

Termination: When all the elements are checked and sorted now we have a sorted portion of the array and it will contains all the elements in array but in the sorted order. Even now the assumption we took at the beginning will remain as true. Which is the “left side sub portion of the array is sorted”.

 

And here we haven’t brought any new variable while the iteration of the loop. What we did is we used the variable we already have and changes the positions. So there is no change in variables.

In summary, Loop invariant is a statement which remains true for each iteration of the loop until the end which proves that the algorithm is theoretically correct.

 

Mathanraj Sharma
University of Jaffna