mergesort_list.mlw 1.29 KB
 Jean-Christophe Filliatre committed Apr 03, 2011 1 2 3 `````` (* Sorting a list of integers using mergesort *) `````` Jean-Christophe Filliatre committed Dec 29, 2010 4 ``````module M `````` 5 `````` `````` Jean-Christophe Filliatre committed Dec 30, 2010 6 `````` use import int.Int `````` 7 `````` use import list.Length `````` Jean-Christophe Filliatre committed Sep 15, 2011 8 `````` use import list.SortedInt `````` 9 10 11 `````` use import list.Append use import list.Permut `````` Andrei Paskevich committed Oct 13, 2012 12 13 14 15 16 17 18 19 20 21 `````` let split (l0 : list 'a) requires { length l0 >= 2 } ensures { let (l1, l2) = result in 1 <= length l1 /\ 1 <= length l2 /\ permut l0 (l1 ++ l2) } = let rec split_aux (l1 : list 'a) l2 l variant { length l } requires { length l2 = length l1 \/ length l2 = length l1 + 1 } ensures { let r1, r2 = result in (length r2 = length r1 \/ length r2 = length r1 + 1) /\ permut (r1 ++ r2) (l1 ++ (l2 ++ l)) } = match l with `````` Jean-Christophe Filliatre committed Apr 03, 2011 22 23 24 25 26 `````` | 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 27 `````` `````` Andrei Paskevich committed Oct 13, 2012 28 29 30 31 `````` let rec merge l1 l2 variant { length l1 + length l2 } requires { sorted l1 /\ sorted l2 } ensures { sorted result /\ permut result (l1 ++ l2) } = match l1, l2 with `````` Jean-Christophe Filliatre committed Apr 03, 2011 32 33 34 35 36 `````` | Nil, _ -> l2 | _, Nil -> l1 | Cons x1 r1, Cons x2 r2 -> if x1 <= x2 then Cons x1 (merge r1 l2) else Cons x2 (merge l1 r2) end `````` 37 `````` `````` Andrei Paskevich committed Oct 13, 2012 38 39 40 `````` let rec mergesort l variant { length l } ensures { sorted result /\ permut result l } = match l with `````` Jean-Christophe Filliatre committed Apr 03, 2011 41 42 `````` | Nil | Cons _ Nil -> l | _ -> let l1, l2 = split l in merge (mergesort l1) (mergesort l2) `````` 43 44 `````` end `````` Jean-Christophe Filliatre committed Dec 29, 2010 45 ``end``