(**************************************************************************) (* *) (* 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@) }