(** {1 MPRI lecture 2-36-1 "Proof of Programs"} *)

(** {2 Binary search, with 32-bit machine integers} *)

module Int32

  use export int.Int
  use export int.ComputerDivision

  function min_int: int = -2147483648
  function max_int: int =  2147483647
  predicate in_int32 (n:int) =  min_int <= n <= max_int

  type int32
  val function of_int32 int32 : int
  axiom bounded: forall x:int32. in_int32 (of_int32 x)

  val cst32 (x:int): int32
    requires  { in_int32 x }
    ensures { of_int32 result = x }

  val add32 (x y:int32): int32
    requires { in_int32 (of_int32 x + of_int32 y) }
    ensures { of_int32 result = of_int32 x + of_int32 y }

  val sub32 (x y:int32): int32
    requires { in_int32 (of_int32 x - of_int32 y) }
    ensures { of_int32 result = of_int32 x - of_int32 y }

  val mul32 (x y:int32): int32
    requires { in_int32 (of_int32 x * of_int32 y) }
    ensures { of_int32 result = of_int32 x * of_int32 y }

  val div32 (x y:int32): int32
    requires { of_int32 y <> 0 }
    requires { in_int32 (div (of_int32 x) (of_int32 y)) }
    ensures { of_int32 result = div (of_int32 x) (of_int32 y) }

end


module BinarySearch

  use int.Int
  use Int32
  use array.Array

  predicate sorted (a: array int) =
    forall i j:int. 0 <= i <= j < length a -> a[i] <= a[j]

  exception Break int32
  exception Not_found

  val a:array int

  let binary_search (v: int)
    requires { in_int32 a.length }
    requires { sorted a }
    ensures { 0 <= of_int32 result < a.length }
    ensures { a[of_int32 result] = v }
    raises { Not_found -> forall i:int. 0 <= i < a.length -> a[i] <> v }
  =
    try
      let ref l = cst32 0 in
      let ref u = sub32 (cst32 a.length) (cst32 1) in
      while of_int32 l <= of_int32 u do
        variant { 0 }
        invariant { true }
        let m = (div32 (add32 u l) (cst32 2)) in
        if a[of_int32 m] < v then
          l <- add32 m (cst32 1)
        else if a[of_int32 m] > v then
          u <- sub32 m (cst32 1)
        else
          raise (Break m)
      done;
      raise Not_found
    with Break i -> i
    end

end



(*
Local Variables:
compile-command: "why3 ide bin_search_int32.mlw"
End:
*)