Wiki Agenda Contact Version française

Insertion sort (lists)

Sorting a list of integers using insertion sort.


Authors: Jean-Christophe Filliâtre

Topics: List Data Structure / Sorting Algorithms

Tools: Why3

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


(* Sorting a list of integers using insertion sort *)

module InsertionSort

  type elt
  predicate le elt elt

  clone relations.TotalPreOrder with type t = elt, predicate rel = le
  clone export list.Sorted      with type t = elt, predicate le  = le,
   goal Transitive.Trans

  use import list.List
  use import list.Permut

  let rec insert (x: elt) (l: list elt) : list elt
    requires { sorted l }
    ensures  { sorted result }
    ensures  { permut (Cons x l) result }
    variant  { l }
  = match l with
    | Nil -> Cons x Nil
    | Cons y r -> if le x y then Cons x l else Cons y (insert x r)
    end

  let rec insertion_sort (l: list elt) : list elt
    ensures { sorted result }
    ensures { permut l result }
    variant { l }
  = match l with
    | Nil -> Nil
    | Cons x r -> insert x (insertion_sort r)
    end

end

download ZIP archive