## Algorithm 63 (partition)

Hoare's Algorithm 63

Auteurs: Jean-Christophe Filliâtre

Catégories: Array Data Structure / Ghost code

Outils: Why3

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

```module Algo63

use int.Int
use ref.Refint
use array.Array
use array.ArrayPermut

(* we pass m and n (as ghost arguments) to ensure [permut_sub];
this will help solvers in the proof of partition *)
let exchange (a: array int) (ghost m n: int) (i j: int) =
requires { 0 <= m <= i <= n < length a /\ m <= j <= n }
ensures  { exchange (old a) a i j }
ensures  { permut_sub (old a) a m (n+1) }
let v = a[i] in
a[i] <- a[j];
a[j] <- v;
assert { exchange (old a) a i j }

val random (m n: int) : int ensures { m <= result <= n }

let partition_ (a: array int) (m n: int) (i j: ref int) (ghost ghx: ref int)
requires { 0 <= m < n < length a }
ensures  { m <= !j < !i <= n }
ensures  { permut_sub (old a) a m (n+1) }
ensures  { forall r:int. m <= r <= !j -> a[r] <= !ghx }
ensures  { forall r:int. !j < r < !i -> a[r] = !ghx }
ensures  { forall r:int. !i <= r <= n -> a[r] >= !ghx }
=
let f = random m n in
let x = a[f] in
ghx := x;
i := m;
j := n;
let rec up_down () variant { 1 + !j - !i } =
requires { m <= !j <= n /\ m <= !i <= n }
requires { permut_sub (old a) a m (n+1) }
requires { forall r:int. m <= r < !i -> a[r] <= x }
requires { forall r:int. !j < r <= n -> a[r] >= x }
requires { a[f] = x }
ensures  { m <= !j <= !i <= n }
ensures  { permut_sub (old a) a m (n+1) }
ensures  { !i = n \/ a[!i] > x }
ensures  { !j = m \/ a[!j] < x }
ensures  { a[f] = x }
ensures  { forall r:int. m <= r < !i -> a[r] <= x }
ensures  { forall r:int. !j < r <= n -> a[r] >= x }
while !i < n && a[!i] <= x do
invariant { m <= !i <= n }
invariant {forall r: int. m <= r < !i -> a[r] <= x }
variant { n - !i }
incr i
done;
while m < !j && a[!j] >= x do
invariant { m <= !j <= n }
invariant { forall r: int. !j < r <= n -> a[r] >= x }
variant { !j }
decr j
done;
if !i < !j then begin
exchange a m n !i !j;
incr i;
decr j;
up_down ()
end
in
up_down ();
assert { !j < !i \/ !j = !i = m \/ !j = !i = n };
if !i < f then begin exchange a m n !i f; incr i end
else if f < !j then begin exchange a m n f !j; decr j end

let partition (a: array int) (m n: int) (i j: ref int) =
requires { 0 <= m < n < length a }
ensures  { m <= !j < !i <= n }
ensures  { permut_sub (old a) a m (n+1) }
ensures  { exists x: int.
(forall r:int. m <= r <= !j -> a[r] <= x) /\
(forall r:int. !j < r < !i -> a[r] = x) /\
(forall r:int. !i <= r <= n -> a[r] >= x) }
partition_ a m n i j (ref 0)

end
```