Loop Invariant

A loop invariant is a condition or property that is true at the beginning and end of every iteration of a loop. Loop invariants are key to proving correctness of iterative algorithms.

For example, in a linear search:

Java:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
int search(int[] arr, int x) {

  int i = 0;

  // Loop invariant:
  // If x is in arr, then x is in arr[0..i]

  while (i < arr.length) {
    if (arr[i] == x) {
      return i;
    }
    i++;
  }

  return -1;
}

C++:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
int search(vector<int>& arr, int x) {

  int i = 0;

  // Loop invariant: 
  // If x is in arr, then x is in arr[0..i]

  while (i < arr.size()) {
    if (arr[i] == x) {
      return i;
    }
    i++;
  }

  return -1; 
}

Python:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
def search(arr, x):

  i = 0
  # Loop invariant:
  # If x in arr, x is in arr[0..i] 

  while i < len(arr):
    if arr[i] == x:
      return i
    i += 1

  return -1

Loop invariants describe what must remain true before and after each loop iteration for algorithm correctness.