Wiki Agenda Contact Version française

Binary search

Searching a sorted array for a given value, in logarithmic time.

Made famous by Bentley's Programming Pearls.


Authors: Jean-Christophe Filliâtre

Topics: Array Data Structure / Searching Algorithms / Tricky termination / Exceptions

Tools: Why3

References: The VerifyThis Benchmarks

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


(* Binary search

   A classical example. Searches a sorted array for a given value v. *)

module BinarySearch

  use import int.Int
  use import int.ComputerDivision
  use import ref.Ref
  use import array.Array

  (* the code and its specification *)

  exception Break int (* raised to exit the loop *)
  exception Not_found (* raised to signal a search failure *)

  let binary_search (a : array int) (v : int)
    requires { forall i1 i2 : int. 0 <= i1 <= i2 < length a -> a[i1] <= a[i2] }
    ensures  { 0 <= result < length a /\ a[result] = v }
    raises   { Not_found -> forall i:int. 0 <= i < length a -> a[i] <> v }
  = try
      let l = ref 0 in
      let u = ref (length a - 1) in
      while !l <= !u do
        invariant { 0 <= !l /\ !u < length a }
        invariant {
          forall i : int. 0 <= i < length a -> a[i] = v -> !l <= i <= !u }
        variant { !u - !l }
        let m = !l + div (!u - !l) 2 in
        assert { !l <= m <= !u };
        if a[m] < v then
          l := m + 1
        else if a[m] > v then
          u := m - 1
        else
          raise (Break m)
      done;
      raise Not_found
    with Break i ->
      i
    end

end

(* A generalization: the midpoint is computed by some abstract function.
   The only requirement is that it lies between l and u. *)

module BinarySearchAnyMidPoint

  use import int.Int
  use import ref.Ref
  use import array.Array

  exception Break int (* raised to exit the loop *)
  exception Not_found (* raised to signal a search failure *)

  val midpoint (l:int) (u:int) : int
    requires { l <= u } ensures { l <= result <= u }

  let binary_search (a :array int) (v : int)
    requires { forall i1 i2 : int. 0 <= i1 <= i2 < length a -> a[i1] <= a[i2] }
    ensures  { 0 <= result < length a /\ a[result] = v }
    raises   { Not_found -> forall i:int. 0 <= i < length a -> a[i] <> v }
  = try
      let l = ref 0 in
      let u = ref (length a - 1) in
      while !l <= !u do
        invariant { 0 <= !l /\ !u < length a }
        invariant {
          forall i : int. 0 <= i < length a -> a[i] = v -> !l <= i <= !u }
        variant { !u - !l }
        let m = midpoint !l !u in
        if a[m] < v then
          l := m + 1
        else if a[m] > v then
          u := m - 1
        else
          raise (Break m)
      done;
      raise Not_found
    with Break i ->
      i
    end

end

(* binary search using 32-bit integers *)

module BinarySearchInt32

  use import mach.int.Int32
  use import ref.Ref
  use import mach.array.Array32

  (* the code and its specification *)

  exception Break int32 (* raised to exit the loop *)
  exception Not_found   (* raised to signal a search failure *)

  let binary_search (a : array int32) (v : int32)
    requires { forall i1 i2 : int. 0 <= i1 <= i2 < to_int a.length ->
               to_int a[i1] <= to_int a[i2] }
    ensures  { 0 <= to_int result < to_int a.length /\ a[to_int result] = v }
    raises   { Not_found ->
                 forall i:int. 0 <= i < to_int a.length -> a[i] <> v }
  = try
      let l = ref (of_int 0) in
      let u = ref (length a - of_int 1) in
      while !l <= !u do
        invariant { 0 <= to_int !l /\ to_int !u < to_int a.length }
        invariant { forall i : int. 0 <= i < to_int a.length ->
                    a[i] = v -> to_int !l <= i <= to_int !u }
        variant   { to_int !u - to_int !l }
        let m = !l + (!u - !l) / of_int 2 in
        assert { to_int !l <= to_int m <= to_int !u };
        if a[m] < v then
          l := m + of_int 1
        else if a[m] > v then
          u := m - of_int 1
        else
          raise (Break m)
      done;
      raise Not_found
    with Break i ->
      i
    end

end

download ZIP archive