include "arrays.why"

(* A variant of quicksort, with partitioning a la Bentley *)

(* exchange of two elements *)

let swap (t:int array)(i,j:int) =
  { 0 <= i < array_length(t) and 0 <= j < array_length(t) }
  let v = t[i] in
  begin
    t[i] := t[j];
    t[j] := v
  end
  { exchange(t, t@, i, j) }

(* The recursive part of the quicksort algorithm:
   a recursive function to sort between [l] and [r] *)

let rec quick_rec (t:int array) (l,r:int) : unit { variant 1+r-l } =
  { 0 <= l and r < array_length(t) }
  if l < r then 
    let v = t[l] in
    let m = ref l in
    let i = ref (l + 1) in
    begin
      L:
      while !i <= r do
	{ invariant (forall j:int. l < j <= m -> t[j] < v)
                and (forall j:int. m < j <  i -> t[j] >= v)
                and permut(t, t@L, l, r)
                and t[l] = v and l <= m < i and i <= r + 1
          variant 1 + r - i }
        if t[!i] < v then begin m := !m + 1; (swap t !i !m) end;
        i := !i + 1
      done;
      (swap t l !m);
      (quick_rec t l (!m - 1));
      (quick_rec t (!m + 1) r)
    end
  { sorted_array(t, l, r) and permut(t, t@, l, r) }

(* At last, the main program, which is just a call to [quick_rec] *)

let quicksort (t:int array) =
  {} 
  (quick_rec t 0 ((array_length_ t)-1))
  { sorted_array(t, 0, array_length(t)-1) and permutation(t, t@) }

(*
Local Variables: 
compile-command: "gwhy quicksort2.mlw"
End: 
*)