Are you preparing for a technical interview? Whether you are applying to be a coding engineer or a software developer, you will need to deal with complex loops that form the building blocks of algorithms involving many logical steps. 

The logic within loops can become difficult to keep track of and understand, especially if you are writing a complex loop. Because of this, writing loops that fail to achieve their goals or fail to terminate is not an uncommon occurrence for software engineers.

This article focuses on the loop invariant, which will help you while writing complex, iterative code. We will learn:

• What Is a Loop Invariant?
• Loop Invariant Properties
• The Difference Between Loop Invariant Condition and Loop Conditional
• Loop Invariant Algorithm
• Loop Invariant Condition of Various Algorithms
• Finding a Solid Loop Invariant Condition: Example
• Strengths and Weaknesses of Loop Invariants
• Examples of Problems/Interview Questions on Loop Invariants
• FAQs on Loop Invariants

What Is a Loop Invariant?

A loop invariant is a formal statement about the relationship between variables in a program that is:

1. Necessarily true immediately before the loop is run for the first time (establishing the invariant)
2. And true again just before and just after each iteration of the loop, including the last iteration (maintaining the invariant)
   

The loop invariant may or may not be true within the loop partway through any iteration. In essence, a loop invariant is a condition that is true for every iteration of the loop: before the loop starts, at the end of each iteration, at the starting of each iteration, and after the loop’s termination.

Loop Invariant Properties

A strong loop invariant satisfies three properties:

• Initialization: The loop invariant condition should be true before the first iteration of the loop.
• Maintenance: If the loop invariant condition is true at the start of an iteration, it must be true at the end of that iteration.
• Termination: The loop invariant condition should give some useful information after the loop is terminated. 

To check if we created a good loop invariant condition and that the algorithm is correct, we do a loop invariant proof. This invariant proof involves checking if all the three above-mentioned properties of a loop invariant are satisfied. If so, the algorithm is correct, and the loop will reach its desired goal after it terminates.

The Difference Between Loop Invariant Condition and Loop Conditional

The loop invariant condition doesn’t involve the loop conditional (test condition of the loop). The invariant is picked so that when the loop conditional becomes false, and the loop terminates, we can be sure that the goal has been reached.

Loop Invariant Algorithm

A typical loop Invariant algorithm would follow this template:

...

...

// The Loop Invariant Condition should be true here

// The loop has a goal it was designed to logically achieve. 

// With each iteration, our loop moves closer to achieving that goal. 

loop (loop conditional)

 {

      // first line of the loop

      … 

      … 

      // last line of the loop

      // the Loop Invariant condition should be true here in each iteration, including the first and the last

   }

   // After the loop terminates, the loop invariant here should confirm that the goal is reached. (Termination + Loop Invariant => Goal)

   ...

Between the first and last line of the loop, the algorithm should be working towards reaching the loop's goal. Hence, changes may occur in the truth value of the loop invariant between the first and last line of the loop, which isn’t an issue. However, the loop invariant must be such that it guarantees it will be restored in each iteration before repeating the loop.

Coming up with simple invariant conditions that satisfy all three invariant properties takes skill. We try to express it as a mathematical equation or relationship as far as possible. However, if this makes the invariant too complicated, we can stick to clear formal statements representing the invariant.

It helps to consider these questions to come up with a strong loop invariant:

First glance:

• Have we stated the loop invariant explicitly at the beginning? 
• Is the loop variable a part of it?
  

The invariant properties:

• Before the loop’s first iteration, does it satisfy the initialization property? 
• Can it help conclude the final answer expected from the loop? After the termination, does it give us the goal of the loop? 
• In the maintenance step, does it satisfy the maintenance property?
• Is it referring to what happened in earlier iterations when proving maintenance or termination property? (It shouldn’t)
• After the termination of the loop, don’t just see if the invariant holds. Ask, does it say something useful about the algorithm and satisfy the termination property?
  

Other factors:

• If there are multiple loops involved, is it clear which loop it is for?
• Are the indexes and/or index range used correctly in the context of each iteration?
• Does it refer to what the algorithm needs to do and what you’re trying to prove?

Loop Invariant Condition of Various Algorithms

In this section, we’ll cover examples of loop invariants used in different popular algorithms.

Loop Invariant for Adding First n Elements of an Array

We’ll begin with a really simple example of finding and proving a loop invariant.  Consider a loop, whose goal is to add the first n elements of an Array[].

int sum = 0, i=0;
while (i < n)
sum = sum + Array[i];
i++;

The loop invariant for this while loop is: On entering iteration i of the loop, sum = a[0] + a[1] + a[2] + ... + a[i-1] holds. Now, let us do a quick invariant proof by checking if the three properties hold for our loop invariant.

• Initialization: On entering the first iteration, i = 0.  And since i-1 = -1, the sum a[0] + ... + a[i-1] is empty. Hence, the sum of no terms is 0 as initialized.
• Maintenance: On entering iteration i, let us assume that the invariant is true. This means sum = a[0] + a[1] + a[2] + ... + a[i-1]. However, this iteration adds a[i] into sum and then increments i. So the loop invariant is maintained when entering the next iteration. 
• Termination: Loop termination happens only once, in this case, when i = n.  As per the invariant, then sum = a[0] + a[1] + a[2] + ... + a[n-1].  The goal of the loop to find the sum of the first n elements of the array is fulfilled, and the invariant evaluated at termination does give us this goal.
  

Hence, this is a valid loop invariant. Let us now look at the loop invariants of some common sorting algorithms.

Loop Invariant for Selection Sort

Selection sort involves iteratively finding the minimum element from the unsorted part of the array and transferring it to the beginning of the unsorted part.

Pseudocode:

indexMinimum = 0;

for(int i = 0; i< size-1;i++)

{

indexMinimum = i;

for(int j=i+1 to size-1)

If (Array[j]<Array[indexMinimum])

indexMinimum = j;

swap(&Array[indexMinimum], &Array[i]);

} 

Here, in the outer loop, the loop invariant condition is that Array is always sorted for the first i elements. For the inner loop, the loop invariant is that Array[indexMinimum] contains the minimum value from Array[i] to Array[j].

Loop Invariant for Insertion Sort

In insertion sort, we have a sorted sub-list that keeps increasing in size until all elements are sorted. We compare elements with each other sequentially, and any element outside this sorted sub-list has to find its appropriate place in the sub-list and be inserted there to become a part of it. For insertion sort, the loop invariant is: for i-th iteration, the subarray Array[0 to i-1] is always sorted.

Pseudocode:

for (i = 1 to size-1)

{

   sortingBegins = Array[i];

   j = i-1;

   while (j >= 0 and Array[j] > sortingBegins)

   {

      Array[j+1] = Array[j];

      j = j-1;

   }

   Array[j+1] = sortingBegins;

}

Loop Invariant for Bubble Sort

Bubble sort works by iteratively placing the largest element of the unsorted sub-array in the rightmost position of the unsorted sub-array. 

Pseudocode:

for (i = 0 to size-2)         

  for (j = 0 to size-i-2)

       if(Array[j]>Array[j+1]

       swap(Array[j], Array[j+1]);

So, the loop invariant for the outer loop here is that at the end of iteration i, the rightmost i elements are sorted and in their correct place. For the inner loop, after each iteration j, the maximum element of the unsorted part is at index j+1.

Finding a Solid Loop Invariant Condition: Example

With these things in mind, let’s get our hands dirty! In this example, we’ll find and prove the loop invariant ourselves. 

We’re going to find a loop invariant for linear search. In linear search, we linearly check each element in the array to find where the number we want is located.

linearSearch(Array, size, toFind)

1. Set numIsAt to Not-Found

2. For each index i (where i goes from 0 to size-1)

a. If Array[i] == toFind, then set numIsAt == i

3. Return numIsAt

We know that the input array is Array[], and we keep track of the iterations of the loop with the index i. Given what we know, let’s come up with a valid, strong invariant.

Invariant Attempt 1

At the start of the iteration with index i, Array[0] to Array[i-1] does not contain toFind.

At the start of the second iteration at index i=1, the invariant says Array[0] to Array[0] does not contain toFind. This isn’t necessarily true at the beginning of the second iteration, as toFind could be present at Array[0]. So this isn’t a valid loop invariant condition.

Invariant Attempt 2

At the start of the iteration with index i, if Array contains toFind, then Array[numIsAt]==toFind holds.

Here, the invariant doesn’t depend on the loop variable at all. It is just repeating something redundant and uninsightful every iteration — “if the goal of the algorithm is reached, this equation will be true.” This invariant also breaks before the start of the loop. Because, even though the array might contain toFind, Array[numIsAt] = toFind will never hold. It’s not a good loop invariant.

Invariant Attempt 3

At the start of the iteration with index i, if numIsAt is a valid index, then A[numIsAt]== toFind holds; else, Array[0,i) (i.e., from Array[0] to Array[i-1]) does not contain toFind.

We’ve stated the invariant clearly here, it depends on the loop variable i, and for each iteration, the index range seems to be correctly used in the context of that iteration. Let us check the correctness of our invariant.

Initialization

Before the loop begins, numIsAt is set to Not-Found, and hence, is not an index. In this case, the loop invariant says Array[0,0) does not contain toFind, which must be true as Array[0,0) is an empty subarray. This saves us from the error in Attempt 1. The invariant satisfies the initialization property.

Maintenance

The maintenance property says that if the invariant is true in the ith iteration, it will be true before the i+1th iteration. Here, i is the loop counter variable. So, we’re going to evaluate the invariant at the start of iteration i, at the end of iteration i, and prove that the invariant still holds at the end of the iteration. 

At the start of iteration i:

Case 1: If the number toFind is found, then A[numIsAt]== toFind 

This case is independent of i. So, at the end of iteration i, numIsAt is an index — we’ve found the number, and the invariant holds again. 

Case 2: If the number has not been found yet, then values from Array[0] to Array[i-1] must not contain the number toFind. 

Since Case 1 is not true, Array[i] does not contain toFind, and Case 2 is true. This means Array[0] to Array[i-1] does not contain toFind. We can now say that Array[0] to Array[i] does not contain toFind. 

At the end of the iteration i:

i goes to i+1; the invariant then says that Array[0] to Array[i+1-1] does not contain toFind, which we just showed is true. Thus, the invariant holds at the starting of the next iteration i+1 and satisfies the maintenance property.

Termination

At the end, i=size — the loop terminates, as it’s run for i=0 to size-1. The loop invariant then becomes: if numIsAt is an index, then A[numIsAt]== toFind; else, Array[0,size) (i.e., from Array[0] to Array[size-1]) does not contain toFind.

We can conclude that the loop invariant at the termination is correct and the invariant holds. Then, the loop invariant at termination tells us that once the loop has entirely run, if the array had that number, it would be found at index numIsAt, or the array does not contain that number at all, which is the goal of the linear search algorithm. Hence, our loop invariant proof shows the correctness of our invariant. We can also claim that the invariant was a strong one as it helped us to reach our goal upon the termination of the loop.

Strengths and Weaknesses of Loop Invariants

Strengths:

1. It can help determine and maintain the correctness of complex logic-based code. It can help programmers ensure the algorithm remains correct even after modifying it (or debug it). They can achieve this by making sure they don’t break the invariant with their changes.
2. Since loop invariants give useful information about why the algorithm works, a comment above a complicated loop that states its loop invariant can help other programmers understand the algorithm being run without going into much detail about the logic running inside the algorithm loop. 
3. It reduces the need to “prove the loop is working” to just “prove the loop invariant is restored with each pass of the loop.” 
   

Weaknesses:

1. Creating loop invariants is unnecessary extra work in the case of simple loops, where the logic is easily understandable.

Examples of Interview Questions/Problems on Loop Invariants

If you are preparing for a technical interview at FAANG or other Tier-1 tech companies, learning loop invariants will not only help you write solid code for any problem, but you will also be able to solve problems or questions specific to loop invariants. Here are a few examples:

1. Implement the following algorithms in C++ and find loop invariant conditions for the loops in them: Merge sort, Quicksort, Binary search, Heap sort.
2. What are the things one should consider to find a strong loop invariant?
3. How can you prove the correctness of an algorithm using loop invariants?
4. What are the properties of a loop invariant?

FAQs on Loop Invariants

Question 1. Are loop invariants unique for each loop?

No. There can be many loop invariants for a loop, although not all of them are useful. A useful, strong loop invariant is essential to prove the correctness of an algorithm using it.

Question 2. When there are multiple loops, how is the loop invariant calculated?

In the case of multiple loops, an invariant is calculated for each loop separately. In the case of nested loops, loop invariants can be found starting from the innermost loop and moving outwards.

Question 3. Should the loop invariant condition hold during the body of the loop as well?

No. The loop invariant condition must be true before the loop starts, before each iteration of the loop, and after the loop terminates. It can be temporarily false within the body of the loop.

Ready to Nail Your Next Coding Interview?

Nailing tech interviews at FAANG and Tier-1 tech companies can be challenging even for seasoned software engineers. It requires a deep understanding of data structure and algorithms as well as systems design. 

If you’re looking for guidance and help to nail these questions and more, sign up for our free webinar. As pioneers in the field of technical interview prep, we have trained thousands of software engineers to crack the toughest coding interviews and land jobs at their dream companies, such as Google, Facebook, Apple, Netflix, Amazon, and more!

Sign up now!

----------

Article contributed by Tanya Shrivastava