/* Quicksort (no permutation property) */ /*@ requires \valid_index(t,i) && \valid_index(t,j) @ assigns t[i],t[j] @ ensures t[i] == \old(t[j]) && t[j] == \old(t[i]) @*/ void swap(int t[],int i,int j); /*@ predicate sorted(int t[], int i, int j) { @ \forall int k; i <= k < j => t[k] <= t[k+1] @ } @*/ /*@ requires 0 <= l && (l <= r => \valid_range(t,l,r)) @ assigns t[l..r] @ ensures sorted(t,l,r) @*/ void quick_rec(int t[], int l, int r) { if (l < r) { int v = t[l]; int m = l; int i = l + 1; L:/*@ invariant @ (\forall int j; l < j <= m => t[j] < v) && @ (\forall int j; m < j < i => t[j] >= v) && @ t[l] == v && l <= m < i <= r + 1 @ loop_assigns @ t[l..r] @ variant @ 1 + r - i @*/ while (i <= r) { if (t[i] < v) { m++; swap(t, i, m); } i++; } swap(t, l, m); quick_rec(t, l, m - 1); quick_rec(t, m + 1, r); } } /* At last, the main program, which is just a call to quick_rec */ /*@ requires n >= 1 && \valid_range(t,0,n-1) @ ensures sorted(t,0,n-1) @*/ void quicksort(int t[], int n) { quick_rec(t, 0, n-1); }