Wiki Agenda Contact English version

Find a value in a sorted list of integers


Auteurs: Jean-Christophe Filliâtre

Catégories: List Data Structure

Outils: 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 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

download ZIP archive