include "arrays.why"

(* Search in an array for a null value *)

exception Not_found

parameter t : int array

(* 1. With a loop. As soon as we find it, we raise (Found i) *)

exception Found of int

let search1 () = 
  {} 
  try
    let i = ref 0 in begin
    while !i < (array_length_ t) do
      { invariant 0 <= i and forall k:int. 0 <= k < i -> t[k] <> 0
        variant array_length(t) - i } 
      if t[!i] = 0 then raise (Found !i);
      i := !i + 1
    done;
    raise Not_found : int
    end 
  with Found x ->
    x
  end
  { t[result] = 0 
  | Not_found => forall k:int. 0 <= k < array_length(t) -> t[k] <> 0 }


(* 1. With a loop. As soon as we find it, we raise Break *)

exception Break

let search2 () = 
  {} 
  let i = ref 0 in 
  try
    begin
    while !i < (array_length_ t) do
      { invariant 0 <= i and forall k:int. 0 <= k < i -> t[k] <> 0
        variant array_length(t) - i }
      if t[!i] = 0 then raise Break;
      i := !i + 1
    done;
    raise Not_found : int
    end 
  with Break ->
    !i
  end
  { t[result] = 0 
  | Not_found => forall k:int. 0 <= k < array_length(t) -> t[k] <> 0 }


(* 3. With a recursive function *)

let search3 () =
  { 0 <= array_length(t) }
  (let rec search_rec (i:int) : int { variant array_length(t) - i } =
     { 0 <= i <= array_length(t) }
     (if i = (array_length_ t) then raise Not_found : int
      else if t[i] = 0 then i
      else (search_rec (i + 1)))
     { t[result] = 0 
     | Not_found => forall k:int. i <= k < array_length(t) -> t[k] <> 0 }
   in
  (search_rec 0))
  { t[result] = 0 
  | Not_found => forall k:int. 0 <= k < array_length(t) -> t[k] <> 0 }