The ProVal team was stopped at the end of August 2012, and reborn into a new team Toccata

## Quicksort (arrays)

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

Authors: Jean-Christophe Filliâtre

Tools: Why3

```
(* 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
```