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

(** {2 Binary Search in an Array *)

use int.Int
use int.ComputerDivision
use array.Array

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

predicate _TO_BE_COMPLETED
constant _VARIANT_TO_BE_COMPLETED:int
(* replace all occurrences of _TO_BE_COMPLETED below *)

let binary_search (a : array int) (v: int)
  requires { _TO_BE_COMPLETED }
  ensures { _TO_BE_COMPLETED }
  =
    let ref l = 0 in
    let ref u = a.length - 1 in
    let ref res = -1 in
    while res < 0 && l <= u do
        invariant { _TO_BE_COMPLETED }
        variant { _VARIANT_TO_BE_COMPLETED }
        let m = div (u + l) 2 in
        if a[m] < v then l <- m+1
        else if a[m] > v then u <- m-1
        else res <- m
      done;
    res




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