examples/insertion_sort_list.mlw

   1
   2 (* Sorting a list of integers using insertion sort *)
   3
   4 module InsertionSort
   5
   6   type elt
   7   val predicate le elt elt
   8
   9   clone relations.TotalPreOrder with
  10     type t = elt, predicate rel = le, axiom .
  11   clone export list.Sorted with
  12     type t = elt, predicate le  = le, goal Transitive.Trans
  13
  14   use list.List
  15   use list.Permut
  16
  17   let rec insert (x: elt) (l: list elt) : list elt
  18     requires { sorted l }
  19     ensures  { sorted result }
  20     ensures  { permut (Cons x l) result }
  21     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   let rec insertion_sort (l: list elt) : list elt
  28     ensures { sorted result }
  29     ensures { permut l result }
  30     variant { l }
  31   = match l with
  32     | Nil -> Nil
  33     | Cons x r -> insert x (insertion_sort r)
  34     end
  35
  36 end