(** {1 MPRI lecture 2-36-1 "Proof of Programs"} *) (** {2 Linear search} *) use int.Int use array.Array (** assumed equality program function on real numbers *) val eq (x y:real) : bool ensures { result <-> x=y } let search (a: array real) (v:real) requires { true } ensures { true } = let ref i = 0 in let ref res = (-1) in while i < a.length do invariant { true } variant { 0 } let t = a[i] in if eq t v then res <- i; i <- i + 1 done; res (* Local Variables: compile-command: "why3 ide lin_search.mlw" End: *)