Wiki Agenda Contact Version française

Binary Sort

Binary sort is a variant of insertion sort where binary search is used to find the insertion point.


Authors: Jean-Christophe Filliâtre

Topics: Array Data Structure / Sorting Algorithms / Algorithms

Tools: Why3

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


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: M.map int 'a) (mid k: int) (x: 'a) : unit
    requires { 0 <= mid <= k }
    requires { forall i. mid < i <= k -> M.get m2 i = M.get m1 (i - 1) }
    requires { M.get m2 mid = M.get m1 k }
    ensures  { M.Occ.occ x m1 mid (k+1) = M.Occ.occ x m2 mid (k+1) }
  = for i = mid to Int.(-) 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 (M.get m1 k) m1 mid (k+1) =
             1 + M.Occ.occ (M.get m1 k) m1 mid k };
    assert { M.Occ.occ (M.get m1 k) m2 mid (k+1) =
             1 + M.Occ.occ (M.get 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 = M.get m1 k \/ x <> M.get 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

download ZIP archive

Why3 Proof Results for Project "binary_sort"

Theory "binary_sort.BinarySort": fully verified

ObligationsAlt-Ergo 1.30CVC4 1.4CVC4 1.5
VC occ_shift---0.54---
VC binary_sort---------
split_goal_right
VC binary_sort.00.01------
VC binary_sort.10.01------
VC binary_sort.20.00------
VC binary_sort.30.01------
VC binary_sort.40.00------
VC binary_sort.50.00------
VC binary_sort.60.00------
VC binary_sort.70.02------
VC binary_sort.80.02------
VC binary_sort.90.02------
VC binary_sort.100.01------
VC binary_sort.110.03------
VC binary_sort.120.01------
VC binary_sort.130.02------
VC binary_sort.140.04------
VC binary_sort.150.00------
VC binary_sort.160.01------
VC binary_sort.170.00------
VC binary_sort.180.01------
VC binary_sort.190.50------
VC binary_sort.20------0.06
VC binary_sort.21---------
introduce_premises
VC binary_sort.21.0---------
case (j=k)
VC binary_sort.21.0.01.50------
VC binary_sort.21.0.10.80------
VC binary_sort.22------0.06
VC binary_sort.230.00------
VC binary_sort.240.00------
VC binary_sort.250.00------