This is the first post in a series that will cover all the fundamental Algorithms and Datastructures.

Loop Invariants

Before looking at our first Algorithm, we need to understand a component of proving an Algorithm functions as intended.

A loop invariant is used to establish correctness that an algorithm will produce correct outputs and maintain certain conditions during the execution of the algorithm.

A loop invariant, as the name indicates uses a loop to execute part of the algorithm with the intention of maintaining an unchanging condition - the invariant.

Loop Invariants are defined in three parts:

1. Initialization: The invariant is true up to the first iteration or up to a certain index. Essentially saying, the invariant holds true before the main loop starts but could also be true when being applied to an array of size 1.
2. Maintenance: The invariant is true before an iteration of the loop and will remain true after the next iteration of the loop.
3. Termination: When the loop terminates, the invariant remains true, demonstrating the correctness of the algorithm.

The Initialization and Maintenance phases act as our base case and inductive step.

Benefits of using Loop Invariants

• Defines a goal with constraints that help clarify algorithmic goals and outcomes
• Encourages reducing the problem down to its smallest element and solving from the ground up. E.g. ensuring initialization holds true for an array of size 1 or 2.
• Formal proof on the correctness of the algorithm.

Example: Finding the Maximum Element in an Array

arr = {4, 2, 7, 8, 1};
v = arr[0]

1. Initialization:

• A variable v will contain the max value seen so far in the array

2. Maintenance:

• Before the first iteration, we have the max value so far

  • v will assigned the value at index 0 (in this case 4)

• After the first iteration, we either update the max value or leave the max value

• This invariant holds on subsequent iterations

3. Termination:

• At the end of the loop, we will have the max value of the whole loop

Example: Find an element in an Array

1. Initialization:

• Up to each index, if v exists, we will have found the value

2. Maintenance:

• Before the next iteration, up to that index, we haven’t found v. After the next iteration, up to that index, we either find v and return the index or continue

3. Termination:

• If we haven’t found v up to the last index, then we return -1

Example: Moving all zeros to the end of the array while preserving order

1. Initialization:

• Up to the current index, all non-zeros will be appear in preserved order, followed by zeros

2. Maintenance:

• Before the first iteration all non-zeros will appear before a zero

• We will use a pointer write_idx which points to the position where the next non-zero value should be placed, increment each time we find a non-zero

• After an iteration, if a non-zero has been found:

  • Assign the current value at write_idx
  • Assign the value at write_idx to current index
  • Increment write_idx

• The array up to the current index, should have all non-zeros appear in preserved order followed by zeros

3. Termination:

• At the end of all zeros should appear after preserved ordered non-zero numbers

Here is the code example for this Invariant:

#include <stdbool.h>
#include <stdio.h>

bool zeros_after_num(int *arr, int arr_size) {
  if (arr == NULL)
    return false;

  if (arr_size < 1)
    return false;

  int write_idx = 0;
  for (int i = 0; i < arr_size; i++) {
    if (arr[i] > 0) {
      int tmp = arr[write_idx];

      arr[write_idx] = arr[i];
      arr[i] = tmp;

      write_idx++;
    }
  }

  return true;
}

Insertion Sort

Let’s take the loop invariant approach and apply it to a well known sorting algorithm.

#include <stdbool.h>
#include <stdio.h>

int insertion_sort(int *arr, int size) {
  if (arr == NULL)
    return false;

  if (size < 2)
    return false;

  for (int i = 1; i < size; i++) {
    int curr_val = arr[i];
    int prev_idx = i - 1;

    while (prev_idx >= 0 && arr[prev_idx] > curr_val) {
      arr[prev_idx + 1] = arr[prev_idx];
      prev_idx--;
    }

    arr[prev_idx + 1] = curr_val;
  }

  return true;
}

int main() {

  int arr[6] = {31, 41, 59, 26, 41, 58};
  #int expected[6] = {26, 31, 41, 41, 58, 59};

  int arr_size = sizeof(arr) / sizeof(arr[0]);
  insertion_sort(arr, arr_size);

  return 0;
}

Initialization

• Up to the current index, the array will be sorted in ascending order

Maintenance

Before commencing the first loop, we established the loop invariant is true - from index 0 to 1, the list is sorted since theres only 1 value.

When we execute the next iteration of the loop.

  for (int i = 1; i < size; i++) {
    int curr_val = arr[i];
    int prev_idx = i - 1;

    while (prev_idx >= 0 && arr[prev_idx] > curr_val) {
      arr[prev_idx + 1] = arr[prev_idx];
      prev_idx--;
    }

    arr[prev_idx + 1] = curr_val;

  }

This inner loop is effectively, iterating backwards from the current index of i towards the start of the loop, checking if there are larger values than the current value.

Within the while loop, we have determined that if there is a larger value than current, indicating the list is unsorted:

• assign the value at prev_idx to prev_idx + 1, effectively right shifting the larger value
• decrement prev_idx

Out of the while loop:

• assign the current value (the smaller value) to the final position, effectively move it to its final position in the array for this iteration.

At the end of the first iteration we have satisfied the Maintenance aspect - before the iteration it was true that the list was sorted, after the iteration the list is still sorted.

This loop invariant will continue for each iteration of the loop.

Termination

When the loop terminates, the invariant should still hold meaning the whole list has now been sorted

Did you find this page helpful? Consider sharing it 🙌