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

(** {2 Linear search, using a for loop} *)

use int.Int
use array.Array

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

let linear_search (a: array int) (v:int)
  requires { _TO_BE_COMPLETED }
  ensures  { _TO_BE_COMPLETED }
= let ref res = (-1) in
  for i = 0 to a.length - 1 do
    invariant { _TO_BE_COMPLETED }
    let t = a[i] in
    if t = v then res <- i
  done;
  res

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