Contact Version française

The ProVal team was stopped at the end of August 2012, and reborn into a new team Toccata
These pages do not evolve anymore, please follow the link above for up-to-date informations about our team.

Quicksort (arrays)

Sorting an array using quicksort, with partitioning a la Bentley.


Authors: Jean-Christophe Filliâtre

Topics: Array Data Structure / Sorting Algorithm / Tricky termination

Tools: Why3

index



(* Sorting an array using quicksort, with partitioning a la Bentley.

   We simply scan the segment l..r from left ro right, maintaining values
   smaller than t[l] on the left part of it (in l+1..m).
   Then we swap t[l] and t[m] and we are done. *)

module Quicksort

  use import int.Int
  use import ref.Ref
  use import array.Array
  use import array.ArraySorted
  use import array.ArrayPermut
  use import array.ArrayEq

  let swap (t:array int) (i:int) (j:int)
    requires { 0 <= i < length t /\ 0 <= j < length t }
    ensures { exchange (old t) t i j }
  = let v = t[i] in
    t[i] <- t[j];
    t[j] <- v

  let rec quick_rec (t:array int) (l:int) (r:int) : unit variant { 1+r-l }
    requires { 0 <= l /\ r < length t }
    ensures { sorted_sub t l (r+1) /\ permut_sub (old t) t l (r+1) }
  = if l < r then begin
      let v = t[l] in
      let m = ref l in
'L:   for i = l + 1 to r do
        invariant { (forall j:int. l < j <= !m -> t[j] < v) /\
                    (forall j:int. !m < j <  i -> t[j] >= v) /\
                    permut_sub (at t 'L) t l (r+1) /\
                    t[l] = v /\ l <= !m < i }
        if t[i] < v then begin m := !m + 1; swap t i !m end
      done;
      swap t l !m;
      quick_rec t l (!m - 1);
      quick_rec t (!m + 1) r
    end

  let quicksort (t : array int) =
    ensures { sorted t /\ permut (old t) t }
    quick_rec t 0 (length t - 1)

end

download ZIP archive