why3/examples/sorted_list.mlw

(* Find a value in a sorted list of integers *)

module FindInSortedList

  use int.Int
  use list.List
  use list.Mem
  use list.SortedInt

  lemma Sorted_not_mem:
    forall x y : int, l : list int.
    x < y -> sorted (Cons y l) -> not mem x (Cons y l)

  let rec find x l
    requires { sorted l }
    variant { l }
    ensures { result=True <-> mem x l }
  = match l with
    | Nil -> False
    | Cons y r -> x = y || x > y && find x r
    end

end