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

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

use int.Int
use array.Array


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