/* * 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 (December 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]: int) { var: int 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]: int) { 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]: int) { var: int pivot; int 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]: int) { var: int diff, sp;; diff = end - start; if (diff <= 1) return; sp = split(start, end, vec); sort_range (start, sp, vec); sort_range (sp, end, vec); return; } unit main () { var: int i, n, x, vec[];; n = 10; vec = alloc(n, 0); for (i = 0; i < n; i = i + 1) { vec[i] = (n - i) * ( n + i); } sort_range(0, 10, vec); return; }