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 val predicate le elt elt clone relations.TotalPreOrder with type t = elt, predicate rel = le, axiom . clone export list.Sorted with type t = elt, predicate le = le, goal Transitive.Trans use list.List use 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