(** {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 { true } ensures { true } = let ref l = 0 in let ref u = length a - 1 in let ref res = -1 in while res < 0 && l <= u do invariant { true } variant { 0 } 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: *)