Selection Sort

SelectionSort.java demonstrates the use of loop invariants to implement selection sort.

Selection sort places an array of integers into ascending order by repeatedly selecting the largest integer out of the array. A boundary index is set up dividing the array into a top region and a bottom region. As we select the largest remaining element from the bottom region we place it into the top region. It is the smallest element yet in the top region so we make room for it by swapping it with the top-most element of the bottom region, and move down the boundary index by one.

There are two opportunities for loop invariants. First, in the method findIndexOfMax(). The loop works its way through the array, each pass considering one more element in the array. We test whether the newly considered element is larger than any previously considered element, and if so, this index is stored in maxIndexSoFar, updating the previously value.

The second use of a loop invariant is in the method selectionSort(). Here the invariant states what's true about each of the two regions separated by the boundary startOfSortedElements.

What often requires attention to detail is whether bounds are strict or not, that is, whether a statement is made about integers up to but not including some limit, or up to and including that limit. Getting those right could make the code simpler. Changing your mind in the middle of implementing could make the code wrong.

The golden rule is of loop invariants is:

Loop Invariant + Termination = Goal The loop invariant is chosen so that it is easily satisfied before the top of the loop, and it is equivalent to reaching the goal when the loop is exited. For example, we have the index of the largest element in some part of the array. At first the part is just element zero. We grow the region step by step, and termination is when the region is the entire array.