mergesort_array.mlw 9.74 KB
Newer Older
1

2
(** {1 Sorting arrays using mergesort}
3 4 5 6

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

7 8
(** {2 Parameters} *)

9
module Elt
10 11

  use export int.Int
12 13 14 15
  use export array.Array

  type elt

16
  val predicate le elt elt
17

18
  clone relations.TotalPreOrder with
19
    type t = elt, predicate rel = le, axiom .
20

21 22
  clone export array.Sorted with type
    elt = elt, predicate le = le, axiom .
23 24 25

end

26 27 28 29 30 31 32
(** {2 Merging}

    It is well-known than merging sub-arrays in-place is extremely difficult
    (we don't even know how to do it in linear time).
    So we use some extra storage i.e. we merge two segments of a first array
    into a second array. *)

33 34
module Merge

35
  clone export Elt with axiom .
36 37
  use export ref.Refint
  use export array.Array
38
  use map.Occ
39 40
  use export array.ArrayPermut

41 42 43 44 45 46 47
  (* merges tmp[l..m[ and tmp[m..r[ into a[l..r[ *)
  let merge (tmp a: array elt) (l m r: int) : unit
    requires { 0 <= l <= m <= r <= length tmp = length a }
    requires { sorted_sub tmp l m }
    requires { sorted_sub tmp m r }
    ensures  { sorted_sub a l r }
    ensures  { permut tmp a l r }
48
    ensures  { forall i: int.
49
               (0 <= i < l \/ r <= i < length a) -> a[i] = (old a)[i] }
50
  = let i = ref l in
51 52 53 54
    let j = ref m in
    for k = l to r-1 do
      invariant { l <= !i <= m <= !j <= r }
      invariant { !i - l + !j - m = k - l }
55 56 57
      invariant { sorted_sub a l k }
      invariant { forall x y: int. l <= x < k -> !i <= y < m -> le a[x] tmp[y] }
      invariant { forall x y: int. l <= x < k -> !j <= y < r -> le a[x] tmp[y] }
58
      invariant { forall v: elt.
59
                  occ v tmp.elts l !i + occ v tmp.elts m !j = occ v a.elts l k }
60
      invariant { forall i: int.
61
                  (0 <= i < l \/ r <= i < length a) -> a[i] = (old a)[i] }
62 63
      if !i < m && (!j = r || le tmp[!i] tmp[!j]) then begin
        a[k] <- tmp[!i];
64 65
        incr i
      end else begin
66
        a[k] <- tmp[!j];
67 68 69 70
        incr j
      end
    done

71 72 73 74 75 76 77 78 79 80 81 82 83 84
  (* merges a[l..m[ and a[m..r[ into a[l..r[, using tmp as a temporary *)
  let merge_using (tmp a: array elt) (l m r: int) : unit
    requires { 0 <= l <= m <= r <= length tmp = length a }
    requires { sorted_sub a l m }
    requires { sorted_sub a m r }
    ensures  { sorted_sub a l r }
    ensures  { permut (old a) a l r }
    ensures  { forall i: int.
               (0 <= i < l \/ r <= i < length a) -> a[i] = (old a)[i] }
  = if l < m && m < r then (* both sides are non empty *)
      if le a[m-1] a[m] then (* OPTIM: already sorted *)
        assert { forall i1 i2: int. l <= i1 < m -> m <= i2 < r ->
                 le a[i1] a[m-1] && le a[m] a[i2] }
      else begin
85
        label N in
86 87
        blit a l tmp l (r - l);
        merge tmp a l m r;
88
        assert { permut_sub (a at N) a l r }
89 90
      end

91 92
end

93 94 95 96
(** {2 Top-down, recursive mergesort}

    Split in equal halves, recursively sort the two, and then merge. *)

97 98
module TopDownMergesort

99 100
  clone Merge with axiom .
  use mach.int.Int
101

102
  let rec mergesort_rec (a tmp: array elt) (l r: int) : unit
103 104 105
    requires { 0 <= l <= r <= length a = length tmp }
    ensures { sorted_sub a l r }
    ensures { permut_sub (old a) a l r }
106
    variant { r - l }
107 108 109 110 111 112 113 114 115
  = if l >= r-1 then return;
    let m = l + (r - l) / 2 in
    assert { l <= m < r };
    mergesort_rec a tmp l m;
    assert { permut_sub (old a) a l r };
    label M in
    mergesort_rec a tmp m r;
    assert { permut_sub (a at M) a l r };
    merge_using tmp a l m r
116

117
  let mergesort (a: array elt) : unit
118 119 120
    ensures { sorted a }
    ensures { permut_all (old a) a }
  =
121
    let tmp = Array.copy a in
122 123 124 125
    mergesort_rec a tmp 0 (length a)

end

126 127 128 129 130 131 132 133
(** {2 Bottom-up, iterative mergesort}

    First sort segments of length 1, then of length 2, then of length 4, etc.
    until the array is sorted.

    Surprisingly, the proof is much more complex than for natural mergesort
    (see below). *)

134 135
module BottomUpMergesort

136 137 138
  clone Merge with axiom .
  use mach.int.Int
  use int.MinMax
139 140

  let bottom_up_mergesort (a: array elt) : unit
141 142
    ensures { sorted a }
    ensures { permut_all (old a) a }
143
  = let n = length a in
144 145 146
    let tmp = Array.copy a in
    let len = ref 1 in
    while !len < n do
147
      invariant { 1 <= !len }
148
      invariant { permut_all (old a) a }
149 150
      invariant { forall k: int. let l = k * !len in
                  0 <= l < n -> sorted_sub a l (min n (l + !len)) }
151
      variant   { 2 * n - !len }
152
      label L in
153
      let lo = ref 0 in
154
      let ghost i = ref 0 in
155
      while !lo < n - !len do
156
        invariant { 0 <= !lo /\ !lo = 2 * !i * !len }
157
        invariant { permut_all (a at L) a }
158 159 160 161
        invariant { forall k: int. let l = k * !len in
                    !lo <= l < n -> sorted_sub a l (min n (l + !len)) }
        invariant { forall k: int. let l = k * (2 * !len) in
                    0 <= l < !lo -> sorted_sub a l (min n (l + 2 * !len)) }
162 163
        variant   { n + !len - !lo }
        let mid = !lo + !len in
164 165
        assert { mid = (2 * !i + 1) * !len };
        assert { sorted_sub a !lo (min n (!lo + !len)) };
166
        let hi = min n (mid + !len) in
167
        assert { sorted_sub a mid (min n (mid + !len)) };
168
        label M in
169
        merge_using tmp a !lo mid hi;
170 171
        assert { permut_sub (a at M) a !lo hi };
        assert { permut_all (a at M) a };
172 173 174
        assert { hi = min n (!lo + 2 * !len) };
        assert { sorted_sub a !lo (min n (!lo + 2 * !len)) };
        assert { forall k: int. let l = k * !len in mid + !len <= l < n ->
175 176
                   sorted_sub (a at M) l (min n (l + !len)) &&
                   sorted_sub a        l (min n (l + !len)) };
177 178 179 180
        assert { forall k: int. let l = k * (2 * !len) in 0 <= l < mid + !len ->
                   k <= !i &&
                   (k < !i ->
                     min n (l + 2 * !len) <= !lo &&
181 182
                     sorted_sub (a at M) l (min n (l + 2 * !len)) &&
                     sorted_sub a        l (min n (l + 2 * !len)) )
183 184
                   &&
                   (k = !i ->
185
                     l = !lo /\ sorted_sub a l (min n (l + 2 * !len)))
186 187 188
               };
        lo := mid + !len;
        ghost incr i
189
      done;
190 191 192 193 194 195 196 197 198 199 200
      assert { forall k: int. let l = k * (2 * !len) in 0 <= l < n ->
               l = (k * 2) * !len &&
               (l < !lo ->
                 sorted_sub a l (min n (l + 2 * !len))) &&
               (l >= !lo ->
                 sorted_sub a l (min n (l + !len)) &&
                 min n (l + 2 * !len) = min n (l + !len) = n &&
                 sorted_sub a l (min n (l + 2 * !len))) };
      len := 2 * !len;
    done;
    assert { sorted_sub a (0 * !len) (min n (0 + !len)) }
201

202 203
end

204 205 206 207 208 209
(** {2 Natural mergesort}

    This is a mere variant of bottom-up mergesort above, where
    we start with ascending runs (i.e. segments that are already sorted)
    instead of starting with single elements. *)

210 211
module NaturalMergesort

212 213 214
  clone Merge with axiom .
  use mach.int.Int
  use int.MinMax
215

216
  (* returns the maximal hi such that a[lo..hi[ is sorted *)
217 218 219 220
  let find_run (a: array elt) (lo: int) : int
    requires { 0 <= lo < length a }
    ensures  { lo < result <= length a }
    ensures  { sorted_sub a lo result }
221
    ensures  { result < length a -> not (le a[result-1] a[result]) }
222 223 224 225 226 227 228 229 230 231 232
  =
    let i = ref (lo + 1) in
    while !i < length a && le a[!i - 1] a[!i] do
      invariant { lo < !i <= length a }
      invariant { sorted_sub a lo !i }
      variant   { length a - !i }
      incr i
    done;
    !i

  let natural_mergesort (a: array elt) : unit
233 234
    ensures { sorted a }
    ensures { permut_all (old a) a }
235
  = let n = length a in
236
    if n <= 1 then return;
237
    let tmp = Array.copy a in
238
    let ghost first_run = ref 0 in
239
    while true do
240
      invariant { 0 <= !first_run <= n && sorted_sub a 0 !first_run }
241
      invariant { permut_all (old a) a }
242
      variant   { n - !first_run }
243
      label L in
244 245 246
      let lo = ref 0 in
      while !lo < n - 1 do
        invariant { 0 <= !lo <= n }
247
        invariant { !first_run at L <= !first_run <= n }
248
        invariant { sorted_sub a 0 !first_run }
249 250
        invariant { !lo = 0 \/ !lo >= !first_run > !first_run at L }
        invariant { permut_all (a at L) a }
251 252
        variant   { n - !lo }
        let mid = find_run a !lo in
253
        if mid = n then begin if !lo = 0 then return; break end;
254
        let hi = find_run a mid in
255
        label M in
256
        merge_using tmp a !lo mid hi;
257 258
        assert { permut_sub (a at M) a !lo hi };
        assert { permut_all (a at M) a };
259 260
        ghost if !lo = 0 then first_run := hi;
        lo := hi;
261 262 263
      done
    done

264 265 266 267 268 269 270 271 272 273 274 275 276 277 278

  (** an alternative implementation suggested by Martin Clochard,
      mixing top-down recursive and natural mergesort

      the purpose is to avoid unnecessary calls to [find_run] in
      the code above *)

  let rec naturalrec (tmp a: array elt) (lo k: int) : int
    requires { 0 <= lo <= length a = length tmp }
    requires { 0 <= k }
    ensures  { result = length a \/ lo + k < result < length a }
    ensures  { sorted_sub a lo result }
    ensures  { permut_sub (old a) a lo (length a) }
    ensures  { forall j: int. 0 <= j < lo -> a[j] = (old a)[j] }
    variant  { k }
279
  = let n = length a in
280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297
    if lo >= n-1 then return n;
    let mid = ref (find_run a lo) in
    if !mid = n then return n;
    for i = 0 to k-1 do
      invariant { lo + i < !mid < n }
      invariant { sorted_sub a lo !mid }
      invariant { permut_sub (old a) a lo (length a) }
      invariant { forall j: int. 0 <= j < lo -> a[j] = (old a)[j] }
      let hi = naturalrec tmp a !mid i in
      assert { permut_sub (old a) a lo (length a) };
      label M in
      merge_using tmp a lo !mid hi;
      assert { permut_sub (a at M) a lo hi };
      assert { permut_sub (a at M) a lo (length a) };
      mid := hi;
      if !mid = n then return n
    done;
    !mid
298 299 300 301 302 303 304 305 306

  let natural_mergesort2 (a: array elt) : unit
    ensures { sorted a }
    ensures { permut_all (old a) a }
  =
    let tmp = Array.copy a in
    let _ = naturalrec tmp a 0 (length a) in
    ()

307
end