(* Binary search

   A classical example. Searches a sorted array for a given value v.
   Consult <https://gitlab.inria.fr/why3/why3/-/blob/master/examples/binary_search.mlw>.
 *)

module BinarySearch

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

  let binary_search (a : array int) (v : int) : int
    requires { forall i1 i2 : int. 0 <= i1 < i2 < length a -> a[i1] <= a[i2] }
    ensures  { 0 <= result <= length a }
    ensures  { forall i: int. 0 <= i < result -> a[i] < v }
    ensures  { forall i: int. result <= i < length a -> v <= a[i] }
  =
    (* IMPORTANT: DON'T MODIFY THE ABOVE LINES *)
    let ref l = 0 in
    let ref r = length a in
    while l < r do
        invariant { 0 <= l <= length a /\ 0 <= r <= length a }
        invariant { forall i: int. 0 <= i < l -> a[i] < v }
        invariant { forall i: int. r <= i < length a -> a[i] >= v }
        variant { r - l }
        let m = l + div (r - l) 2 in
        assert { l <= m < r };
        if a[m] < v then
            l := m + 1
        else
            r := m
    done;
    l

end