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