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

(** {2 Binary search} *)


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

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

val a : array int

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



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