(*** Algorithm 64 C. A. R. Hoare Elliott Brothers Ltd., Hertfordshire, England, U.K. Communications of the ACM archive Volume 4 , Issue 7 (July 1961) table of contents Pages: 321 - 322 ***) module Algo64 use import int.Int use import ref.Ref use import array.Array use import array.ArrayPermut use import array.ArraySorted (* Algorithm 63 *) val partition (a:array int) (m:int) (n:int) (i:ref int) (j:ref int) : unit requires { 0 <= m < n < length a } writes {a,i,j} ensures { m <= !j < !i <= n } ensures { permut_sub (old a) a m (n+1) } ensures { exists x:int. (forall r:int. m <= r <= !j -> a[r] <= x) /\ (forall r:int. !j < r < !i -> a[r] = x) /\ (forall r:int. !i <= r <= n -> a[r] >= x) } (* Algorithm 64 *) let rec quicksort (a:array int) (m:int) (n:int) : unit variant { n-m } = requires { 0 <= m <= n < length a } ensures { permut_sub (old a) a m (n+1) } ensures { sorted_sub a m (n+1) } 'Init: if m < n then begin let i = ref 0 in let j = ref 0 in partition a m n i j; 'L1: quicksort a m !j; assert { permut_sub (at a 'L1) a m (n+1) }; 'L2: quicksort a !i n; assert { permut_sub (at a 'L2) a m (n+1) } end end