insertion_sort_list.mlw 837 Bytes
Newer Older
1 2 3

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

4
module InsertionSort
5

6
  type elt
7
  val predicate le elt elt
8

9
  clone relations.TotalPreOrder with
10 11 12
    type t = elt, predicate rel = le, axiom .
  clone export list.Sorted with
    type t = elt, predicate le  = le, goal Transitive.Trans
13

14 15
  use list.List
  use list.Permut
16

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

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

36
end