insertion_sort_list.mlw 788 Bytes
Newer Older
1 2 3

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

4
module InsertionSort
5

6 7 8 9 10
  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
11 12
  use import list.Permut

13
  let rec insert (x: elt) (l: list elt) : list elt
14
    requires { sorted l }
15 16 17
    ensures  { sorted result }
    ensures  { permut (Cons x l) result }
    variant  { l }
18
  = match l with
19
    | Nil -> Cons x Nil
20
    | Cons y r -> if le x y then Cons x l else Cons y (insert x r)
21
    end
22

23 24 25 26
  let rec insertion_sort (l: list elt) : list elt
    ensures { sorted result }
    ensures { permut l result }
    variant { l }
27
  = match l with
28 29 30
    | Nil -> Nil
    | Cons x r -> insert x (insertion_sort r)
    end
31

32
end