Loop invariants

The title might be new to some readers, but believe me, if you are a coder then you may have already used this concept somewhere around. Isn’t that great! Implementing something you are totally unaware of.

Now is the time to know the concept. So that you can get the utmost benefit of it.

Like warriors have their armour to fight! We, the coders have algorithms to solve any given problem! (just trying to be funny! 😅).

This article includes the following sub-topics:

1. What is loop invariant? (obviously!)
2. Example of loop invariant. (to keep this concept in our brains!)
3. Usage. (after all, we have to use it!)

“An algorithm is a well-defined computational procedure that takes some value, or set of values, as input and produces some values, or set of values, as output.”

-from Introduction to algorithms (CLRS)

In simpler words:

An algorithm is a procedure to follow to get the desired output for some provided input.

1. What is loop invariant?

Most of the algorithms, have loops in them. What if I say that these loop invariants play a vital role in making loops (at the end, algorithms) successful!?

A loop invariant is a formal statement about the relationship between variables that hold immediately before and immediately after each iteration of a loop. (“Invariant” means “not varying” or “not changing”)

While loop conditional is the condition which controls the termination of the loop.

The following is the general pattern of Loop invariants:

…
 // the Loop Invariant must be true here
 for ( TEST CONDITION ) {
 // top of the loop
 …
 …
 // bottom of the loop
 // the Loop Invariant must be true here
 }
…

We must show the following three properties of loop invariant:

1. Initialization: The loop invariant must be true before the first execution of the loop.
2. Maintenance: If the invariant is true before an iteration of the loop, it should be true also after the iteration.
3. Termination: When the loop is terminated the invariant should tell us something useful, something that helps us understand the algorithm.

(it can be temporarily false during the body of the loop.)

While loop conditional must be false after the loop terminates, otherwise the loop would never terminate.

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 i.e.,

invariant + termination = goal

2. Example of loop invariant.

In insertion sort, loop invariant condition is that the subarray A[0 to i-1] is always sorted. Here, the parameter is an array A[0 . . n] of length n.

//insertion sort
for (i = 1 to n-1)
{
   key = arr[i];
   j = i-1;
   //insert A[i] into the sorted sequence A[0 .. i-1]
   while (j >= 0 and arr[j] > key)
   {
      arr[j+1] = arr[j];
      j = j-1;
   }
   arr[j+1] = key;
}

The following is the explanation:

I designed this using Canva. Hope you liked it. :-)

This is how the loop invariant holds for all three properties.

3. Usage

• Loop invariants can be used to prove the correctness of an algorithm, debug an existing algorithm without even tracing the code.
• Trial and method can be used to write easy algorithms but it is better to use formal methods like loop invariants when the complexity of the problem increases. In this way, loop invariants are used to reason about the correctness of computer programs.
• A loop Invariant can help in the design of iterative algorithms.

References :

[1]Book: Introduction to Algorithms (CLRS)

[2]https://www.cs.miami.edu/home/burt/learning/Math120.1/Notes/LoopInvar.html

[3] https://www.geeksforgeeks.org/loop-invariant-condition-examples-sorting-algorithms/

Hi! I am Srishti. I am new to this platform and this is my first article. Thank you for reading it. I really hope that it helped you gain some more knowledge.

Last but not least, every opinion and suggestion is wholeheartedly welcome in the comment section below.

Contact details:

LinkedIn: www.linkedin.com/in/srishti-kanojia-704607151

Twitter: https://twitter.com/SrishtiKanojia5