## 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: 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

download ZIP archive

# Why3 Proof Results for Project "binary_sort"

## Theory "binary_sort.BinarySort": fully verified

Obligations | Alt-Ergo 2.0.0 | CVC4 1.4 | |||

VC for occ_shift | --- | 0.54 | |||

VC for binary_sort | --- | --- | |||

split_vc | |||||

loop invariant init | 0.00 | --- | |||

loop invariant init | 0.00 | --- | |||

index in array bounds | 0.00 | --- | |||

loop invariant init | 0.01 | --- | |||

loop invariant init | 0.00 | --- | |||

loop invariant init | 0.00 | --- | |||

precondition | 0.00 | --- | |||

index in array bounds | 0.01 | --- | |||

loop variant decrease | 0.01 | --- | |||

loop invariant preservation | 0.02 | --- | |||

loop invariant preservation | 0.01 | --- | |||

loop invariant preservation | 0.01 | --- | |||

loop variant decrease | 0.01 | --- | |||

loop invariant preservation | 0.02 | --- | |||

loop invariant preservation | 0.00 | --- | |||

loop invariant preservation | 0.01 | --- | |||

precondition | 0.00 | --- | |||

precondition | 0.00 | --- | |||

index in array bounds | 0.01 | --- | |||

assertion | --- | --- | |||

inline_goal | |||||

assertion | --- | --- | |||

split_vc | |||||

assertion | 0.02 | --- | |||

assertion | 2.31 | --- | |||

assertion | 0.02 | --- | |||

assertion | 0.01 | --- | |||

loop invariant preservation | 1.81 | --- | |||

loop invariant preservation | 0.03 | --- | |||

postcondition | 0.01 | --- | |||

postcondition | 0.00 | --- | |||

out of loop bounds | 0.01 | --- |