examples/binary_sort.mlw

   1
   2 (** Binary sort
   3
   4     Binary sort is a variant of insertion sort where binary search is used
   5     to find the insertion point. This lowers the number of comparisons
   6     (from N^2 to N log(N)) and thus is useful when comparisons are costly.
   7
   8     For instance, Binary sort is used as an ingredient in Java 8's
   9     TimSort implementation (which is the library sort for Object[]).
  10
  11     Author: Jean-Christophe Filliâtre (CNRS)
  12 *)
  13
  14 module BinarySort
  15
  16   use int.Int
  17   use int.ComputerDivision
  18   use ref.Ref
  19   use array.Array
  20   use array.ArrayPermut
  21
  22   let lemma occ_shift (m1 m2: int -> 'a) (mid k: int) (x: 'a) : unit
  23     requires { 0 <= mid <= k }
  24     requires { forall i. mid < i <= k -> m2 i = m1 (i - 1) }
  25     requires { m2 mid = m1 k }
  26     ensures  { M.Occ.occ x m1 mid (k+1) = M.Occ.occ x m2 mid (k+1) }
  27   = for i = mid to k - 1 do
  28       invariant { M.Occ.occ x m1 mid i = M.Occ.occ x m2 (mid+1) (i+1) }
  29       ()
  30     done;
  31     assert { M.Occ.occ (m1 k) m1 mid (k+1) =
  32              1 + M.Occ.occ (m1 k) m1 mid k };
  33     assert { M.Occ.occ (m1 k) m2 mid (k+1) =
  34              1 + M.Occ.occ (m1 k) m2 (mid+1) (k+1) };
  35     assert { M.Occ.occ x m1 mid (k+1) = M.Occ.occ x m2 mid (k+1)
  36              by x = m1 k \/ x <> m1 k }
  37
  38   let binary_sort (a: array int) : unit
  39     ensures { forall i j. 0 <= i <= j < length a -> a[i] <= a[j] }
  40     ensures { permut_sub (old a) a 0 (length a) }
  41   =
  42     for k = 1 to length a - 1 do
  43       (* a[0..k-1) is sorted; insert a[k] *)
  44       invariant { forall i j. 0 <= i <= j < k -> a[i] <= a[j] }
  45       invariant { permut_sub (old a) a  0 (length a) }
  46       let v = a[k] in
  47       let left = ref 0 in
  48       let right = ref k in
  49       while !left < !right do
  50         invariant { 0 <= !left <= !right <= k }
  51         invariant { forall i. 0      <= i < !left -> a[i] <= v        }
  52         invariant { forall i. !right <= i < k     ->         v < a[i] }
  53         variant   { !right - !left }
  54         let mid = !left + div (!right - !left) 2 in
  55         if v < a[mid] then right := mid else left := mid + 1
  56       done;
  57       (* !left is the place where to insert value v
  58          so we move a[!left..k) one position to the right *)
  59       label L in
  60       self_blit a !left (!left + 1) (k - !left);
  61       a[!left] <- v;
  62       assert { permut_sub (a at L) a !left (k + 1) };
  63       assert { permut_sub (a at L) a 0 (length a) };
  64     done
  65
  66 end