(** {1 MPRI lecture 2-36-1 "Proof of Programs"} *) (** {2 Linear Search in an Array *) 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 i = 0 in let ref res = -1 in while i < a.length do invariant { _TO_BE_COMPLETED } variant { _VARIANT_TO_BE_COMPLETED } let t = a[i] in if t = v then res <- i; i <- i + 1 done; res (* Local Variables: compile-command: "why3 ide lin_search.mlw" End: *)