insertion_sort_list.mlw 838 Bytes
Newer Older
1 2 3

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

4
module InsertionSort
5

6 7 8 9
  type elt
  predicate le elt elt

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

13
  use import list.List
14 15
  use import list.Permut

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

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

35
end