l < r:

1. small < r not an invariant: if all items in the partition range are smaller than the pivot, after the last loop iteration small = r. 2. small < large: not an invariant for the same reason as above. 3. small <= large: this is an invariant: before the loop executed small < large (because l < r) and after the last iteration, small = large. 4. for all i such that l <= i < small, arr[i] < pivot: this is a loop invariant. Before the loop is executed, there are no such i. After each iteration, items to the left of small are less than the pivot. 5. for all j such that large <= j <= r, arr[j] >= pivot: this is a loop invariant. Before the loop is executed, large = r and the value at this index is the pivot, so arr[j] = pivot. After each iteration, items at the index large and to the right are greater or equal to the pivot. 6. for all j such that large < j <= r, arr[j] >= pivot: this is also a loop invariant. It is a weaker statement than 5 so if 5 is true then 6 is true.

void selectionSort(int arr[], int len){ int i; int j; int temp; int pos_greatest; for( i = len - 1; i > 0; i--){ pos_greatest = 0; for(j = 0; j <= i; j++){ if( arr[j] > arr[pos_greatest]){ pos_greatest = j; }//end if }//end inner for loop temp = arr[i]; arr[i] = arr[pos_greatest]; arr[pos_greatest] = temp; }//end outer for loop }//end selection sort

Proof:

- true before the first iteration (no numbers before position 0)
- Suppose it is true at the start of iteration j, namely for all k < j, arr[k] <= arr[pos_greatest]. Now we look at arr[j]. If it is greater than arr[pos_greatest] we reset pos_greatest to be j and it now holds the index of the greatest number between 0 and j (inclusive). Otherwise we just increment j and again pos_greatest holds the index of the greatest number between 0 and j (inclusive). So in either case we have for all k <= j, arr[k] <= arr[pos_greatest]. After we increment j this becomes again for all k < j, arr[k] <= arr[pos_greatest].

When the inner loop terminates, i < j. So the invariant of the inner loop implies that for all k <= i, arr[k] <= arr[pos_greatest], in other words, pos_greatest is the index of the greatest item between 0 and i (inclusive).

Proof that this property is an invariant of the outer loop:

- before the first passage through the loop: there are no k with i < k <= len - 1, so the statement is trivially true.
- Suppose that the property is true before the iteration when i
equals say x. We need to show that the same property will be true
after the iteration when i will be equal x-1.

Before the iteration we had:

(1) for all k with x < k, arr[k] <= arr[k+1]<=... <= arr[n-1]

(all numbers strictly to the right of x are ordered)

and

(2) for all k with x < k and for all m with m <= x, arr[m] <= arr[k].

(all numbers to the left of x including x are smaller than the numbers on the right)

All that happens in the iteration is: the inner loop executes and finds the index of the greatest number between 0 and x (inclusive). That number is then swapped to the position x. From (2) we know that this number is smaller than all numbers to the right of x and from (1) we know that those numbers are ordered in ascending order, so now we have

(1') for all k with x <= k, arr[k] <= arr[k+1]<=... <= arr[n-1]

(all numbers to the right of x including x are ordered)

We also know that the number at x is the greatest in the range from 0 to x, so we have (2') for all k with x <= k and for all m with m < x, arr[m] <= arr[k]

(all numbers to the left of x are smaller than the numbers on the right)

Finally the outer loop decrements i so we have to reformulate (1') and (2') for the new value of i which is x-1: (1) for all k with len-1 >= k > i, arr[k] <= arr[k+1]<=... <= arr[n-1]

(all numbers strictly to the right of i are ordered)

(2) for all k with len - 1 >= k > i and for all 0 <= m <= i, arr[m] <= arr[k].

arr[0] <= arr[1] <= ... <= arr[len-1] so the array is sorted.