insertion_sort_list.mlw 585 Bytes
Newer Older
1 2 3

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

4
module M
5

6
  use import int.Int
7
  use import list.Length
8
  use import list.SortedInt
9 10
  use import list.Permut

11 12 13 14
  let rec insert x l variant { l }
    requires { sorted l }
    ensures { sorted result /\ permut (Cons x l) result }
  = match l with
15 16 17
    | Nil -> Cons x Nil
    | Cons y r -> if x <= y then Cons x l else Cons y (insert x r)
    end
18

19 20 21
  let rec insertion_sort l variant { l }
    ensures { sorted result /\ permut l result }
  = match l with
22 23 24
    | Nil -> Nil
    | Cons x r -> insert x (insertion_sort r)
    end
25

26
end