Use of loop invariants in Selection Sort.
Selection sort uses the following code to sort an array x of length n.
We assume
a procedure swap which exchanges the values of its parameters.
The input condition is that there is an
input array x[1] .. x[n], and the
output condition is that the same variables will contain
the sorted permutation of the values of the input array.
for (int i = 1; i < n; i++){
int k = i;
for (int j = i+1; j ≤ n; j++)
if (x[j] < x[k]) k = j;
if (k > i)
swap(x[i],x[k]);
}
We first transform the for loops into while loops.
int i = 1;
while (i < n){
int k = i;
int j = i+1;
while (j ≤ n){
if (x[j] < x[k]) k = j;
j++;
}
if (k > i)
swap(x[i],x[k]);
i++;
}
Since there are two loops, we need two loop invariants.
The purpose of the outer loop is to swap ith smallest element
into x[i], or to do nothing if it is already there. The purpose of the
inner loop is to find the index of that smallest element, by linear search
through the subarrary x[i] .. x[n].
-
OLI = Outer loop invariant: All the items x[1] .. x[i-1] are in their correct
positions.
More formally, the array items are a permutation of the input
array, and, for any 1 ≤ l < i,
x[l] is the lth smallest element of the input array.
-
ILI = Inner loop invariant:
-
The outer loop invariant holds.
-
x[k] is the smallest element in the subarray x[i] .. x[j-1].
![](../CSC456/bluhorsa.gif)