(**************************************************************************)
(*                                                                        *)
(* Proof of the Quicksort Algorithm.                                      *)
(*                                                                        *)
(*  This formal proof is detailed in this paper:                          *)
(*                                                                        *)
(*  J.-C. Filliâtre and N. Magaud. Certification of sorting algorithms    *)
(*  in  the system  Coq. In  Theorem Proving  in Higher  Order Logics:    *)
(*  Emerging Trends, 1999.                                                *)
(*  (http://www.lri.fr/~filliatr/ftp/publis/Filliatre-Magaud.ps.gz)       *)
(*                                                                        *)
(* Jean-Christophe Filliâtre (LRI, Université Paris Sud)                  *)
(* August 1998                                                            *)
(*                                                                        *)
(**************************************************************************)

(* The first part of the program that re-arrange elements in the array
   and returns the position of the "partition" is defined in the module
   [Partition_prog]. *)

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

let quick_rec =
  let rec quick_rec (t:int array)(l,r:int) : unit 
  { variant r-l } =
    { 0 <= l and r < array_length(t) (*as Pre*) }
    (if l < r then
       let p = (partition t l r) in
       begin
       	 (quick_rec t l (p-1));
	 (quick_rec t (p+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 =
  fun (t:int array) ->
    {}
    (quick_rec t 0 ((array_length_ t)-1))
    { sorted_array(t, 0, array_length(t)-1) and permutation(t, t@) }