mergesort_list.mlw 2.51 KB
Newer Older
 Jean-Christophe Filliatre committed Apr 03, 2011 1 2 3 `````` (* Sorting a list of integers using mergesort *) `````` Jean-Christophe Filliatre committed Mar 28, 2014 4 ``````module Elt `````` 5 `````` `````` Jean-Christophe Filliatre committed Mar 28, 2014 6 7 8 9 `````` use export int.Int use export list.Length use export list.Append use export list.Permut `````` 10 `````` `````` Jean-Christophe Filliatre committed Mar 28, 2014 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 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 `````` type elt predicate le elt elt clone relations.TotalPreOrder with type t = elt, predicate rel = le clone export list.Sorted with type t = elt, predicate le = le end module Merge use export Elt let rec merge (l1 l2: list elt) : list elt requires { sorted l1 /\ sorted l2 } ensures { sorted result /\ permut result (l1 ++ l2) } variant { length l1 + length l2 } = match l1, l2 with | Nil, _ -> l2 | _, Nil -> l1 | Cons x1 r1, Cons x2 r2 -> if le x1 x2 then Cons x1 (merge r1 l2) else Cons x2 (merge l1 r2) end end (* TODO: proof to be completed module EfficientMerge use export Elt use import list.Mem use import list.Reverse use import list.RevAppend let rec merge_aux (acc l1 l2: list elt) : list elt requires { sorted (reverse acc) /\ sorted l1 /\ sorted l2 } requires { forall x y: elt. mem x acc -> mem y l1 -> le x y } requires { forall x y: elt. mem x acc -> mem y l2 -> le x y } ensures { sorted result /\ permut result (acc ++ l1 ++ l2) } variant { length l1 + length l2 } = match l1, l2 with | Nil, _ -> rev_append acc l2 | _, Nil -> rev_append acc l1 | Cons x1 r1, Cons x2 r2 -> if le x1 x2 then merge_aux (Cons x1 acc) r1 l2 else merge_aux (Cons x2 acc) l1 r2 end let merge (l1 l2: list elt) : list elt requires { sorted l1 /\ sorted l2 } ensures { sorted result /\ permut result (l1 ++ l2) } = merge_aux Nil l1 l2 end *) module Mergesort use import Merge let split (l0: list 'a) : (list 'a, list 'a) `````` Andrei Paskevich committed Oct 13, 2012 71 `````` requires { length l0 >= 2 } `````` Jean-Christophe Filliatre committed Mar 28, 2014 72 `````` ensures { let (l1, l2) = result in `````` Andrei Paskevich committed Oct 13, 2012 73 `````` 1 <= length l1 /\ 1 <= length l2 /\ permut l0 (l1 ++ l2) } `````` Jean-Christophe Filliatre committed Mar 28, 2014 74 `````` = let rec split_aux (l1 l2 l: list 'a) : (list 'a, list 'a) `````` Andrei Paskevich committed Oct 13, 2012 75 `````` requires { length l2 = length l1 \/ length l2 = length l1 + 1 } `````` Jean-Christophe Filliatre committed Mar 28, 2014 76 `````` ensures { let r1, r2 = result in `````` Andrei Paskevich committed Oct 13, 2012 77 78 `````` (length r2 = length r1 \/ length r2 = length r1 + 1) /\ permut (r1 ++ r2) (l1 ++ (l2 ++ l)) } `````` Jean-Christophe Filliatre committed Mar 28, 2014 79 `````` variant { length l } `````` Andrei Paskevich committed Oct 13, 2012 80 `````` = match l with `````` Jean-Christophe Filliatre committed Apr 03, 2011 81 82 83 84 85 `````` | Nil -> (l1, l2) | Cons x r -> split_aux l2 (Cons x l1) r end in split_aux Nil Nil l0 `````` Jean-Christophe Filliatre committed May 20, 2011 86 `````` `````` Jean-Christophe Filliatre committed Mar 28, 2014 87 `````` let rec mergesort (l: list elt) : list elt `````` Andrei Paskevich committed Oct 13, 2012 88 `````` ensures { sorted result /\ permut result l } `````` Jean-Christophe Filliatre committed Mar 28, 2014 89 `````` variant { length l } `````` Andrei Paskevich committed Oct 13, 2012 90 `````` = match l with `````` Jean-Christophe Filliatre committed Apr 03, 2011 91 92 `````` | Nil | Cons _ Nil -> l | _ -> let l1, l2 = split l in merge (mergesort l1) (mergesort l2) `````` 93 94 `````` end `````` Jean-Christophe Filliatre committed Dec 29, 2010 95 ``end``