Interview Kickstart has enabled over 3500 engineers to uplevel.
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:
A loop invariant is a formal statement about the relationship between variables in a program that is:
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.
A strong loop invariant satisfies three properties:
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 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.
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:
The invariant properties:
In this section, we’ll cover examples of loop invariants used in different popular algorithms.
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];
The loop invariant for this while loop is: On entering iteration i of the loop, sum = a + a + a + ... + a[i-1] holds. Now, let us do a quick invariant proof by checking if the three properties hold for our loop invariant.
Hence, this is a valid loop invariant. Let us now look at the loop invariants of some common sorting algorithms.
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.
indexMinimum = 0;
for(int i = 0; i< size-1;i++)
indexMinimum = i;
for(int j=i+1 to size-1)
indexMinimum = j;
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].
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.
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;
Bubble sort works by iteratively placing the largest element of the unsorted sub-array in the rightmost position of the unsorted sub-array.
for (i = 0 to size-2)
for (j = 0 to size-i-2)
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.
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.
At the start of the iteration with index i, Array to Array[i-1] does not contain toFind.
At the start of the second iteration at index i=1, the invariant says Array to Array does not contain toFind. This isn’t necessarily true at the beginning of the second iteration, as toFind could be present at Array. So this isn’t a valid loop invariant condition.
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.
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 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.
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.
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 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 to Array[i-1] does not contain toFind. We can now say that Array 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 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.
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 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.
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:
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.
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!
Article contributed by Tanya Shrivastava