// precondition: x is an array of base type T with n items
// ie, const int n=XXX; T x[n];
/*
* definition: a list x' is a sorted version of a list x if
* x' contains the same collection of entries reordered to
* respect an ordering condition such as <=.
*
* lemma: if the length of a list x is <= 1, x' = x. I.e., the
* empty list is sorted and any list containing just one item is sorted.
*
* Predicates:
*
* P1: unsorted is the length of the unsorted (or not yet sorted)
* portion of the list x.
*
* P1a: the sublist x[unsorted ... n-1] of length n-unsorted
* is sorted (i.e., properly ordered).
*
* P2: every item in the unsorted portion of x (the sublist
* x[0 ... unsorted-1]) is <= every item in the sorted portion.
*
* P3: maxloc is the index of a maximal item in the unsorted portion.
*
* P4: the item in the last position of the unsorted portion is
* maximal: that is, it is >= all items in the unsorted portion.
*/
// goal: sort the n items in place (i.e., rather than making a new array)
int unsorted = n; // tracks the size of the unsorted portion of x
// now P1 holds. lemma holds always. P2 holds trivially (sorted = 0)
while ( unsorted > 1 )
{
// P1, lemma, P2 and unsorted > 1
// find largest unsorted entry. i.e., _establish_ P3
int maxloc = 0;
for ( int i = 1; i < unsorted; i++ )
if ( x[i] > x[maxloc] )
maxloc = i;
// P1, lemma, P2, unsorted > 1 and P3
// exchange biggest and last items in unsorted portion
T temp = x[maxloc];
x[maxloc] = x[unsorted - 1];
x[unsorted - 1] = temp;
// P3 not necessarily true. P1, lemma, P2, unsorted > 1 and P4
// the exchange operation
// a) establishes P4
// b) invalidates P3
// c) _preserves_ collection(x): exchange changes
// the order but not the "set" of items in x.
// move the sorted/unsorted boundary
unsorted--;
// P1 still holds, unsorted > 1 may not hold
// does P2 still hold? why?
}
// claim: x is now sorted. That is, the array variable x now contains
// a sorted version of the list originally contained in x.