insertion_sort_list.mlw 811 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
  use import list.List
12 13
  use import list.Permut

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

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

33
end