/** * Quick Sort (broken) * This is a spectacularly broken version of QuickSort * that was suggested in class. * You should read and reason about this code carefully and find all the bugs! * RUN: cc0 -x arrayutil.c0 sort-broken.c0 sort-test2.c0 */ int partition(int[] A, int lower, int pivot_index, int upper) //@requires 0 <= lower && lower <= pivot_index && pivot_index < upper && upper <= \length(A); //@ensures lower <= \result && \result < upper; //@ensures le_seg(A[\result], A, lower, \result); //@ensures ge_seg(A[\result], A, \result, upper); { int pivot = A[pivot_index]; swap(A, pivot_index, lower); int left = lower + 1; int right = upper; while (left < right) //@loop_invariant lower <= left && left <= right && right <= upper; //@loop_invariant ge_seg(pivot, A, lower, left); //@loop_invariant le_seg(pivot, A, right, upper); //@loop_invariant pivot == A[lower]; { if (A[left] <= pivot) { left++; } else { //@assert A[left] > pivot; swap(A, left, right); right--; } } //@assert left == right; swap(A, pivot_index, left-1); return left-1; } void sort(int[] A, int lower, int upper) //@requires 0 <= lower && lower <= upper && upper <= \length(A); //@ensures is_sorted(A, lower, upper); { if (upper - lower == 1) return; int pivot_index = lower + (upper - lower) / 2; //@assert lower < pivot_index && pivot_index < upper; int mid = partition(A, lower, pivot_index, upper); sort(A, lower, mid); sort(A, mid, upper); return; }