## Algorithm 64 (quicksort)

Hoare's Algorithm 64

Authors: Jean-Christophe Filliâtre

Tools: Why3

see also the index (by topic, by tool, by reference, by year)

```module Algo64

use int.Int
use ref.Ref
use array.Array
use array.ArrayPermut
use array.IntArraySorted

(* Algorithm 63 *)

val partition (a: array int) (m n: int) (i j: ref int) (ghost x: 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  { forall r:int. m <= r <= !j -> a[r] <= !x }
ensures  { forall r:int. !j < r < !i -> a[r] = !x }
ensures  { forall r:int. !i <= r <= n -> a[r] >= !x }

(* Algorithm 64 *)

predicate qs_partition (t1 t2: array int) (m n i j: int) (x: int) =
permut_sub t1 t2 m (n+1) /\
(forall k:int. m <= k <= j  -> t2[k] <= x) /\
(forall k:int. j <  k <  i  -> t2[k] =  x) /\
(forall k:int. i <= k <= n ->  t2[k] >= x)

let rec quicksort (a:array int) (m n:int) : unit
requires { 0 <= m <= n < length a }
variant  { n - m }
ensures  { permut_sub (old a) a m (n+1) }
ensures  { sorted_sub a m (n+1) }
= if m < n then begin
let i = ref 0 in
let j = ref 0 in
let ghost x = ref 42 in
partition a m n i j x;
label L1 in
quicksort a m !j;
assert { qs_partition (a at L1) a m n !i !j !x };
label L2 in
quicksort a !i n;
assert { qs_partition (a at L2) a m n !i !j !x }
end

let qs (a:array int) : unit
ensures  { permut_all (old a) a }
ensures  { sorted a }
= if length a > 0 then quicksort a 0 (length a - 1)

end
```

download ZIP archive