Loop Invariants

In my previous post we had discussed the Insertion Sort Algorithm and in this post we are going to understand the concept of Loop Invariant with respect to the correctness of Insertion Sort Algorithm.

Loop Invariants :

As the name name suggests , a loop invariant is the property of a loop. We use loop invariant to understand the correctness of Algorithm.

In order to understand Loop Invariant we need to understand Mathematical Induction since it is very closely related to Mathematical Induction.

We all might have studied Mathematical Induction in our school days to prove the correctness of mathematical statements. A very basic example of a mathematical statement that can be proved my induction is mentioned below -

1+2+3+⋯+n=n(n+1)/2 for all n≥1

Mathematical Induction is a mathematical proof technique. It is essentially used to prove that a statement P(n) which is n(n+1)/2 for the above mentioned statement is true for all integers n≥1

In order to prove it we must very if it is true for all the integers with n = 1,2,3....,n i.e it should be true for P(1), P(2), P(3),...,P(n)

A proof by induction basically consists of two cases.

1. A base case or basis - This basically proves that the statement is true for n=1 without assuming any knowledge of other cases. Often the base case is proved by n=1 or with any fixed natural number n=k

2. Inductive Step - This proves that if the statement holds for any given case n=k , then it must also hold for the next case n=k+1

These two steps establish that the statement holds for every natural number n.

Similar to the technique of mathematical induction the Loop Invariants also have a base case and an inductive step, however since the loop also has a termination criteria with itself we have an additional step for Loop Invariants for the termination criteria unlike mathematical induction where we just have 2 steps since there is no termination criteria hence the inductive steps continues till infinity to prove the statement true for all n≥1. In case of Loop Invariants we stop the induction process when the loop terminates.

Thus in order to show the correctness of algorithm we must show three things about a loop invariant.

1. Initialization
2. Maintenance
3. Termination

Let us examine how these properties holds for insertion sort.

1. Initialization – Since we are sorting an array A[1…..n] and j is initialized with 2 in line 1 of the INSERTION-SORT(A) procedure , it indicates that the first iteration of the loop starts with j=2 the array A[1…j-1] which is A[1] for j=2 , should be sorted. The array A[1] is sorted since it has only one element hence the loop invariant holds true prior to the first iteration of the loop.

2. Maintenance – In all the inductive step right from the initialization until the termination the for loop find the correct position for A[j] moving the prior elements to the right and each inductive step do give us an array which is sorted at each iteration thus stating that the maintenance property holds true for the for loop.

3. Termination – The loop terminates when j > A.Length = n when j = n+1 the loop terminates with the Array A having elements 1 … n . Observing that the array A[1….n] is the entire sequence of elements to be sorted in the original array an all of the elements are sorted thus proving the correctness of the insertion sort algorithm.

The concept of mathematical induction appeared to be confusing to me when I first learnt about in school but after doing the proofs for few of the statements using the process of induction I got an understanding of the process.

Similarly the process of Loop Invariants to identify the correctness of an algorithm would be clear if we do the dry run of procedure and try to check the property (Array being Sorted for our insertion sort algorithm) at Initialization , Maintenance and Termination.

Identifying the loop invariant for our loop in an important aspect of using this technique.

Conclusion

We have covered the following points in this basic post -

1. What is Loop Invariant ?
2. Loop Invariant and Mathematical Induction
3. The properties of Loop Invariant

References –

• Wikipedia
• Introduction to Algorithm

Please share the post by clicking the social media icons at the beginning of the post.
Thank you for reading and see you in the next post !👋