/* * This is an example in Xanadu showing that array bounds checking * is not needed for doing quicksort on an array. The code is written * by Hongwei Xi (29 Nov 1999) */ {size:nat, i:nat, j:nat, k:nat | i < size, j < size, k < size} [n:nat | n < size] int(n) median(i:int(i), j:int(j), k:int(k), vec[size]: float) { var: float x, y, z;; x = vec[i]; y = vec[j]; z = vec[k]; if (x >. y) { if (y >. z) return j; else { if (x >. z) return k; else return i; } } else { if (y >. z) { if (x >. z) return i; else return k; } else return j; } } {size:nat, start:nat, end:nat | start < end <= size} [n:nat | n < size] int(n) get_pivot (start: int(start), end: int(end), vec[size]: float) { var: int d, diff; int i, j, k;; diff = end - start; if (diff < 7) return start + (diff / 2); else { i = start; j = start + diff / 2; k = end - 1; if (diff < 40) return median(i, j, k, vec); else { d = diff / 8; i = median(i, i + d, i + 2 * d, vec); j = median(j - d, j, j + d, vec); k = median(k - 2 * d, k - d, k, vec); return median(i, j, k, vec); } } } {size:nat, start: nat, end: nat | start < end <= size} [n:nat | start <= n < end] int(n) split(start: int(start), end: int(end), vec[size]: float) { var: int pivot; float x, temp; l: [i:int | start <= i <= end] int(i); h: [j:int | start <= j < end] int(j);; pivot = get_pivot(start, end, vec); l = start; h = end - 1; x = vec[pivot]; while (true) { while (l < end) { if (vec[l] <=. x) l = l + 1; else break; } while (start < h) { if (vec[h] >. x) h = h - 1; else break; } if (l < h) { temp = vec[l]; vec[l] = vec[h]; vec[h] = temp; l = l + 1; h = h - 1; } else return h; } exit; } {size:nat, start: nat, end: nat | start <= end <= size} unit sort_range (start: int(start), end: int(end), vec[size]: float) { var: int diff, sp;; diff = end - start; if (diff <= 1) { return; } else { sp = split(start, end, vec); sort_range (start, sp, vec); sort_range (sp, end, vec); return; } } {n:nat} unit print_array (size: int(n), a[n]: float) { var: nat i;; for (i = 0; i < size; i = i + 1) { print_float (a[i]); print_string ("\t"); } print_newline (); } unit main () { var: int i, n; float x, vec[];; n = 100; vec = alloc(n, 0.0); invariant: [i:nat] (i: int(i)) for (i = 0; i < n; i = i + 1) { vec[i] = float_of_int ((n - i) * i); } print_array (n, vec); sort_range(0, n, vec); print_array (n, vec); return; }