mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
95 lines
2.8 KiB
Plaintext
95 lines
2.8 KiB
Plaintext
(***
|
|
|
|
Algorithm 63
|
|
|
|
C. A. R. Hoare
|
|
Elliott Brothers Ltd., Hertfordshire, England, U.K.
|
|
|
|
Communications of the ACM archive
|
|
Volume 4 , Issue 7 (July 1961) table of contents
|
|
Pages: 321 - 322
|
|
|
|
***)
|
|
|
|
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
|