quicksort(;b,e) [data_interval(b, e, data)] { local piv, l, r; if (e > b) { piv = b->dta; l = b + 1; r = e; while (l <= r) [data_interval(b,e, _data) * (b < l) * (l <= r + 1) * (r <= e) * ``PERM org_data _data`` * ``HD org_data = HD _data`` * ``!n. (0 < n) /\ (n < l - b) ==> (EL n _data <= piv)`` * ``!n. (r - b < n) /\ (n <= e - b) ==> (piv < EL n _data)``] { c = l->dta; if (c <= piv) { l = l + 1; } else { tmp1=l->dta; tmp2=r->dta; l->dta = tmp2; r->dta = tmp1; r = r - 1; } } tmp1=r->dta; tmp2=b->dta; r->dta = tmp2; b->dta = tmp1; quicksort (;b, r); quicksort (;l, e); } } [data_interval(b, e, _rdata) * ``(SORTED $<= _rdata) /\ (PERM data _rdata)``]