Loop Invariant: algorithm insight

When it comes to computer algorithms, loops are essential. And with loop, comes a fundamental property that must be valid for a successful algorithm design; this property is called Loop Invariant. Take a look at the following pseudo-code for insertion sort:

InsertionSort(Arr):  
  for j = 2 to Arr.length    
    key = Arr[j]    
    i = j - 1    
    while i > 0 and Arr[i] > key
      Arr[i+1] = Arr[i]
      i = i - 1
   Arr[i+1] = key

Here,

1. we start at the index j = 2,
2. store the Arr[j] in the key,
3. then we compare each element from index j -1 to 0 with the key; if the element is greater than the key (the condition) we move the element one step up (Arr[i+1] = Arr[i]) until the condition is satisfied,
4. Once, the condition is broken we find the correct position for the key.

Note that the subarray Arr[j-1] is already sorted before the start of the for loop. This is true because there is only one element before the start of the for loop.

Also, note that subarray Arr[j-1](now the entire array) is also sorted at the end of this for loop.

This is something that never changes throughout every iteration of the loop. We call it the Loop Invariant — property that remains constant from the beginning to end of the loop in an algorithm. In order to show the correctness of any algorithm we must satisfy the following condition about the Loop invariant:

1. Initialization: It must be true before the first iteration of the loop.
2. Maintainance: It must be true before and after each iteration of the loop.
3. Termination: It must be true at the end of the loop. Loop invariant is typically used along with the condition that causes the loop to terminate.