Wiki Agenda Contact Version française

Find a value in a sorted list of integers


Authors: Jean-Christophe Filliâtre

Topics: List Data Structure

Tools: Why3

see also the index (by topic, by tool, by reference, by year)


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

module FindInSortedList

  use import int.Int
  use import list.List
  use import list.Mem
  use import 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

download ZIP archive