include "arrays.why"

logic v : int

function mean(x : int, y : int) : int = (x + y) / 2

axiom mean : forall x,y:int. x <= y -> x <= mean(x,y) <= y

predicate In(t : int farray, l : int, u : int) =
   exists i:int. l <= i <= u and t[i] = v

parameter t : int array

parameter l,u,p,m : int ref

let binary_search () =
  { array_length(t) >= 1 and sorted_array(t,1,array_length(t)-1) }
  begin
    l := 1; u := (array_length_ t)-1; p := 0;
    while !l <= !u do
      { invariant 
	  1 <= l and u <= array_length(t)-1 and 0 <= p <= array_length(t)-1
          and (p = 0 -> In(t,1,array_length(t)-1) -> In(t,l,u))
          and (p > 0 -> t[p]=v)
        variant 2+u-l }
      m := (mean !l !u);
      assert { l <= m and m <= u };
      if t[!m] < v then
        l := !m + 1
      else if t[!m] > v then
        u := !m - 1
      else begin
        p := !m; (* break => *) l := !u + 1
      end       
    done
  end
  { (1 <= p <= array_length(t)-1 and t[p]=v) or 
    (p = 0 and not In(t,1,array_length(t)-1)) }