module BinarySearch
  use bool.Bool
  use int.Int
  use int.ComputerDivision
  use ref.Ref
  use array.Array

  exception Not_found (* raised to signal a search failure *)

  let binary_search (arr: array int) (x: int): int
    requires { forall i1 i2. 0 <= i1 <= i2 < length arr -> arr[i1] <= arr[i2] }
    ensures  { 0 <= result < length arr /\ arr[result] = x }
    raises   { Not_found -> forall i. 0 <= i < length arr -> arr[i] <> x }
  =
    let low = ref (-1) in
    let high = ref (length arr) in

    while !high - !low > 1 do
      variant { !high - !low }
      invariant { -1 <= !low < !high <= length arr }
      invariant { forall i. 0 <= i < length arr -> arr[i] = x -> exists j. 0 <= j < length arr /\ arr[j] = x /\ !low <= j < !high }

      let mid = div (!high + !low) 2 in
      if arr[mid] <= x then
        low := mid
      else
        high := mid
    done;
    if andb (0 <= !low) (!low < length arr) then
      if arr[!low] = x then
        return !low;
    raise Not_found
end

(*
 *  To prove this with why3 and z3, save the code above to a file (say 'bin_search.mlw') and run:
 *
 *  $ why3 prove -P z3 bin_search.mlw
 *  bin_search.mlw BinarySearch VC binary_search: Valid (0.03s)
 *)