mergesort_list.mlw 5.4 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
105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188

module OCamlMergesort

  clone export Elt
  use import list.Mem
  use import list.Reverse
  use import list.RevAppend

  function prefix int (list 'a) : list 'a

  axiom prefix_def1:
    forall l: list 'a. prefix 0 l = Nil
  axiom prefix_def2:
    forall n: int, x: 'a, l: list 'a. n > 0 ->
    prefix n (Cons x l) = Cons x (prefix (n-1) l)

  let rec chop (n: int) (l: list 'a) : list 'a
    requires { 0 <= n <= length l }
    ensures  { l = prefix n l ++ result }
    variant  { n }
  =
    if n = 0 then l else
    match l with
      | Cons _ t -> chop (n-1) t
      | Nil -> absurd
    end

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

  lemma sorted_rev_append: forall acc l: list elt.
    sorted (reverse acc) ->
    sorted l ->
    (forall x y. mem x acc -> mem y l -> le x y) ->
    sorted (reverse (rev_append l acc))

  let rec rev_merge (l1 l2 accu: list elt) : list elt
    requires { sorted (reverse accu) /\ sorted l1 /\ sorted l2 }
    requires { forall x y: elt. mem x accu -> mem y l1 -> le x y }
    requires { forall x y: elt. mem x accu -> mem y l2 -> le x y }
    ensures  { sorted (reverse result) }
    ensures  { permut result (accu ++ l1 ++ l2) }
    variant  { length l1 + length l2 }
  = match l1, l2 with
    | Nil, _ -> rev_append l2 accu
    | _, Nil -> rev_append l1 accu
    | Cons h1 t1, Cons h2 t2 ->
       if le h1 h2 then rev_merge t1 l2 (Cons h1 accu)
                   else rev_merge l1 t2 (Cons h2 accu)
    end

  lemma sorted_reverse_cons2:
    forall x l. sorted (reverse (Cons x l)) -> sorted (reverse l)

  let rec rev_merge_rev (l1 l2 accu: list elt) : list elt
    requires { sorted accu /\ sorted (reverse l1) /\ sorted (reverse l2) }
    requires { forall x y: elt. mem x accu -> mem y l1 -> le y x }
    requires { forall x y: elt. mem x accu -> mem y l2 -> le y x }
    ensures  { sorted result }
    ensures  { permut result (accu ++ l1 ++ l2) }
    variant  { length l1 + length l2 }
  = match l1, l2 with
    | Nil, _ -> rev_append l2 accu
    | _, Nil -> rev_append l1 accu
    | Cons h1 t1, Cons h2 t2 ->
       if not (le h1 h2) then rev_merge_rev t1 l2 (Cons h1 accu)
                         else rev_merge_rev l1 t2 (Cons h2 accu)
    end

  val sort (n: int) (l: list elt) : list elt
    requires { 2 <= n <= length l }
    ensures  { sorted result }
    ensures  { permut result (prefix n l) }

  lemma permut_prefix: forall l: list elt. permut (prefix (length l) l) l

  let mergesort (l: list elt) : list elt
    ensures { sorted result /\ permut result l }
  =
    let n = length l in
    if n < 2 then l else sort n l

end