mergesort_list.mlw 2.77 KB
Newer Older
1

2 3 4 5
(** Sorting a list of integers using mergesort

    Author: Jean-Christophe Filliâtre (CNRS)
*)
6

7
module Elt
8

9 10 11 12
  use export int.Int
  use export list.Length
  use export list.Append
  use export list.Permut
13

14 15 16 17 18 19 20
  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

21
module Merge (* : MergeSpec *)
22

23
  clone export Elt
24 25 26

  let rec merge (l1 l2: list elt) : list elt
    requires { sorted l1 /\ sorted l2 }
27 28
    ensures  { sorted result }
    ensures  { permut result (l1 ++ l2) }
29 30 31 32 33 34 35 36 37 38
    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

39
(** tail recursive implementation *)
40

41 42 43
module EfficientMerge (* : MergeSpec *)

  clone export Elt
44 45 46 47
  use import list.Mem
  use import list.Reverse
  use import list.RevAppend

48 49 50 51
  lemma sorted_reverse_cons:
    forall acc x1. sorted (reverse acc) ->
    (forall x. mem x acc -> le x x1) -> sorted (reverse (Cons x1 acc))

52 53 54 55
  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 }
56 57
    ensures  { sorted result }
    ensures  { permut result (acc ++ l1 ++ l2) }
58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76
    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

77
  clone import Merge
78 79

  let split (l0: list 'a) : (list 'a, list 'a)
80
    requires { length l0 >= 2 }
81
    ensures  { let (l1, l2) = result in
82
      1 <= length l1 /\ 1 <= length l2 /\ permut l0 (l1 ++ l2) }
83
  = let rec split_aux (l1 l2 l: list 'a) : (list 'a, list 'a)
84
      requires { length l2 = length l1 \/ length l2 = length l1 + 1 }
85
      ensures  { let r1, r2 = result in
86 87
        (length r2 = length r1 \/ length r2 = length r1 + 1) /\
        permut (r1 ++ r2) (l1 ++ (l2 ++ l)) }
88
      variant { length l }
89
    = match l with
90 91 92 93 94
      | Nil -> (l1, l2)
      | Cons x r -> split_aux l2 (Cons x l1) r
      end
    in
    split_aux Nil Nil l0
95

96
  let rec mergesort (l: list elt) : list elt
97
    ensures { sorted result /\ permut result l }
98
    variant { length l }
99
  = match l with
100 101
      | Nil | Cons _ Nil -> l
      | _ -> let l1, l2 = split l in merge (mergesort l1) (mergesort l2)
102 103
    end

104
end