mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
67 lines
2.3 KiB
Plaintext
67 lines
2.3 KiB
Plaintext
|
|
(** Binary sort
|
|
|
|
Binary sort is a variant of insertion sort where binary search is used
|
|
to find the insertion point. This lowers the number of comparisons
|
|
(from N^2 to N log(N)) and thus is useful when comparisons are costly.
|
|
|
|
For instance, Binary sort is used as an ingredient in Java 8's
|
|
TimSort implementation (which is the library sort for Object[]).
|
|
|
|
Author: Jean-Christophe Filliâtre (CNRS)
|
|
*)
|
|
|
|
module BinarySort
|
|
|
|
use int.Int
|
|
use int.ComputerDivision
|
|
use ref.Ref
|
|
use array.Array
|
|
use array.ArrayPermut
|
|
|
|
let lemma occ_shift (m1 m2: int -> 'a) (mid k: int) (x: 'a) : unit
|
|
requires { 0 <= mid <= k }
|
|
requires { forall i. mid < i <= k -> m2 i = m1 (i - 1) }
|
|
requires { m2 mid = m1 k }
|
|
ensures { M.Occ.occ x m1 mid (k+1) = M.Occ.occ x m2 mid (k+1) }
|
|
= for i = mid to k - 1 do
|
|
invariant { M.Occ.occ x m1 mid i = M.Occ.occ x m2 (mid+1) (i+1) }
|
|
()
|
|
done;
|
|
assert { M.Occ.occ (m1 k) m1 mid (k+1) =
|
|
1 + M.Occ.occ (m1 k) m1 mid k };
|
|
assert { M.Occ.occ (m1 k) m2 mid (k+1) =
|
|
1 + M.Occ.occ (m1 k) m2 (mid+1) (k+1) };
|
|
assert { M.Occ.occ x m1 mid (k+1) = M.Occ.occ x m2 mid (k+1)
|
|
by x = m1 k \/ x <> m1 k }
|
|
|
|
let binary_sort (a: array int) : unit
|
|
ensures { forall i j. 0 <= i <= j < length a -> a[i] <= a[j] }
|
|
ensures { permut_sub (old a) a 0 (length a) }
|
|
=
|
|
for k = 1 to length a - 1 do
|
|
(* a[0..k-1) is sorted; insert a[k] *)
|
|
invariant { forall i j. 0 <= i <= j < k -> a[i] <= a[j] }
|
|
invariant { permut_sub (old a) a 0 (length a) }
|
|
let v = a[k] in
|
|
let left = ref 0 in
|
|
let right = ref k in
|
|
while !left < !right do
|
|
invariant { 0 <= !left <= !right <= k }
|
|
invariant { forall i. 0 <= i < !left -> a[i] <= v }
|
|
invariant { forall i. !right <= i < k -> v < a[i] }
|
|
variant { !right - !left }
|
|
let mid = !left + div (!right - !left) 2 in
|
|
if v < a[mid] then right := mid else left := mid + 1
|
|
done;
|
|
(* !left is the place where to insert value v
|
|
so we move a[!left..k) one position to the right *)
|
|
label L in
|
|
self_blit a !left (!left + 1) (k - !left);
|
|
a[!left] <- v;
|
|
assert { permut_sub (a at L) a !left (k + 1) };
|
|
assert { permut_sub (a at L) a 0 (length a) };
|
|
done
|
|
|
|
end
|