Loop Invariant Bubble Sort

Bubble Sort

Hello! This is part 7 in a series of short articles on loop invariants. You can refer to the first part (introduction) here. Today, we are going to discuss bubble sort algorithm in the context of loop invariants.

Problem definition

Given an array (A) of (n) numbers. Develop an algorithm to sort the array in increasing order using bubble sort. Recall that bubble sort compares each element with its neighbor to the right then swaps them if they are out of order. The comparison is repeated until all elements in the array are sorted. If you are interested, here is an article about optimizing bubble sort. Here is a schematic diagram that you can refer to as you read through the article:

Identify the goal of the loop and write it as a post condition

The goal of the algorithm is to sort the elements in the array. This means we are going to get another permutation (contains original elements) of the array where each element is less than or equal to its neighbor to the right.

Write the loop specifying the guard (loop condition)

Please note that bubble sort uses two loops so we will have two loop invariants. As in the previous articles, we will be using while loops in our demonstration because it clearly separates the guard (loop condition) from initialization and loop index, however we can use any other kind of loop if we wish (for example a for loop). Here is the skeleton of the while loops along with the post condition from step 1:

Note that the outer loop index (i) decreases until it is equal to (1) and the inner loop index (j) increases until it is equal to (i). This is going to make more sense when we choose an appropriate invariant for each loop.

Fill in the loop invariant

Loop invariant should describe the goal of the algorithm. It should hold true just before entering the loop and after each iteration. It should give an idea about the current progress towards the final goal. In the case of bubble sort we have an outer loop and an inner loop so we have two invariants not only one. We can think of the inner loop as the implementation of the outer loop then only think about the outer loop. After that, we find an appropriate invariant for the inner loop. Imagine the array is split into two sections around some position (i). Assume elements to the right of (i) are sorted and the ones to the left of (i) are not. The inner loop pushes the largest element from the unsorted section to its correct place in the sorted section. On the other hand, the outer loop pushes the position (i) to the left each iteration until all elements are in the correct place. As you can see, as the outer loop progresses, the sorted section grows and the unsorted section shrinks. The outer loop invariant should give us an idea about this sorting progress. Let us try to use the following invariant for the outer loop “Elements to the right of (i) are sorted”. Similarly, the inner loop bubbles up the largest element in the unsorted section to the sorted section on right side of the array. The inner loop invariant should also give us an idea about what the inner loop does so let us use the invariant: “The bubbling element at position (j) in the unsorted section is the greatest element in the first (j) elements”. We will verify that these invariants hold true before and after each iteration in each loop. The following code shows the loops and their invariants in a formal way:

Fix the initialization so that the loop invariant evaluate to true

Let us first work on the outer loop. Before entering the loop there should be no sorted section yet. This means we should initialize (i = n). Apply that to the outer invariant as follows:

The number of array elements in the range (n + 1) to (n) is zero. In other words:

This makes sense because the array is not sorted yet before entering the outer loop. In order to prove that the outer invariant holds true after each iteration, let us test the first iteration when (i = n – 1). Apply that to the invariant:

This means A[n] to the right of (n – 1) is sorted. Now take the second iteration when (i = n – 2) just to be sure:

This means the last two elements in the array are now sorted and in the right place so the invariant holds after each iteration. Now let us see what happens when the outer loop terminates. The outer loop terminates when (i = 1). Apply that to the invariant:

This basically says all elements except the first one are sorted and in the right place. This is nothing but saying the whole are array is now sorted because the first element is in its correct place. In other words the post condition or the goal of the loop has been achieved. Please pay attention that the outer loop index (i) is decremented after the inner loop (not before) otherwise the outer loop invariant will not hold true after the first iteration. The reason why it will not hold true if we do so is because the inner loop is used to push one element at a time from the unsorted section to the sorted section. Here is how:

Apply that you get:

This is not true, how come we claim that the last element in the array A[n] is in its correct place while we did not move any elements yet from the unsorted section to the sorted section. Do not forget that the inner loop moves one element at a time from the unsorted to the sorted section that is why it should precede the statement (i–). Note that our discussion so far was about the outer loop. We assumed the inner loop does its job correctly. Since the inner loop can be viewed as the implementation of the body of the outer loop, let us now initialize the inner loop so that the inner invariant holds true before and after each iteration. Let us initialize (j = 1) and see what is going to happen:

This is trivially true. In the next step will implement the body of the inner loop so that the inner invariant holds true after each iteration and when the loop exits.

Figure out how to achieve the goal by filling in the body of the loop

As we mentioned earlier the job of the inner loop is to bubble the largest element in the unsorted section to the sorted section on the right side of the array. In order to do so we compare the element at position (j) with its neighbor to the right at position (j + 1) then swap them if they are out of order

That is it for today, in the next article we will discuss a new example “Insertion Sort“.

Please use the comments section below for questions, corrections or feedback. Thanks for reading.