mergesort_array.mlw 9.95 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 16 17 18 19
  use export array.Array

  type elt

  predicate le elt elt

  clone relations.TotalPreOrder with type t = elt, predicate rel = le

20
  clone export array.Sorted with type elt = elt, predicate le = le
21 22 23

end

24 25 26 27 28 29 30
(** {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. *)

31 32
module Merge

33
  clone export Elt
34 35 36 37 38
  use export ref.Refint
  use export array.Array
  use import map.Occ
  use export array.ArrayPermut

39 40 41 42 43 44 45
  (* 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 }
46
    ensures  { forall i: int.
47
               (0 <= i < l \/ r <= i < length a) -> a[i] = (old a)[i] }
48 49 50 51 52 53
  = 'L:
    let i = ref l in
    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 }
54 55 56
      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] }
57
      invariant { forall v: elt.
58
                  occ v tmp.elts l !i + occ v tmp.elts m !j = occ v a.elts l k }
59
      invariant { forall i: int.
60 61 62
                  (0 <= i < l \/ r <= i < length a) -> a[i] = (at a 'L)[i] }
      if !i < m && (!j = r || le tmp[!i] tmp[!j]) then begin
        a[k] <- tmp[!i];
63 64
        incr i
      end else begin
65
        a[k] <- tmp[!j];
66 67 68 69
        incr j
      end
    done

70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89
  (* 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
        'N:
        blit a l tmp l (r - l);
        merge tmp a l m r;
        assert { permut_sub (at a 'N) a l r }
      end

90 91
end

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

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

96 97
module TopDownMergesort

98
  clone import Merge
99 100
  use import mach.int.Int

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

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

end

127 128 129 130 131 132 133 134
(** {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). *)

135 136
module BottomUpMergesort

137
  clone import Merge
138 139 140 141
  use import mach.int.Int
  use import int.MinMax

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

204 205
end

206 207 208 209 210 211
(** {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. *)

212 213
module NaturalMergesort

214
  clone import Merge
215 216
  use import mach.int.Int
  use import int.MinMax
217

218
  (* returns the maximal hi such that a[lo..hi[ is sorted *)
219 220 221 222
  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 }
223
    ensures  { result < length a -> not (le a[result-1] a[result]) }
224 225 226 227 228 229 230 231 232 233 234 235 236 237
  =
    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

  exception Break
  exception Return

  let natural_mergesort (a: array elt) : unit
238 239 240
    ensures { sorted a }
    ensures { permut_all (old a) a }
  = 'I:
241
    let n = length a in
242
    if n >= 2 then
243
    let tmp = Array.copy a in
244
    let ghost first_run = ref 0 in
245 246
    try
    while true do
247 248
      invariant { 0 <= !first_run <= n && sorted_sub a 0 !first_run }
      invariant { permut_all (at a 'I) a }
249
      variant   { n - !first_run }
250
      'L:
251 252 253 254
      let lo = ref 0 in
      try
      while !lo < n - 1 do
        invariant { 0 <= !lo <= n }
255 256 257 258
        invariant { at !first_run 'L <= !first_run <= n }
        invariant { sorted_sub a 0 !first_run }
        invariant { !lo = 0 \/ !lo >= !first_run > at !first_run 'L }
        invariant { permut_all (at a 'L) a }
259 260 261 262
        variant   { n - !lo }
        let mid = find_run a !lo in
        if mid = n then begin if !lo = 0 then raise Return; raise Break end;
        let hi = find_run a mid in
263
        'M:
264
        merge_using tmp a !lo mid hi;
265 266
        assert { permut_sub (at a 'M) a !lo hi };
        assert { permut_all (at a 'M) a };
267 268
        ghost if !lo = 0 then first_run := hi;
        lo := hi;
269 270 271 272 273
      done
      with Break -> () end
    done
    with Return -> () end

274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319

  (** 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 }
  = 'I:
    let n = length a in
    if lo >= n-1 then n else
    try
      let mid = ref (find_run a lo) in
      if !mid = n then raise Break;
      for i = 0 to k-1 do
        invariant { lo + i < !mid < n }
        invariant { sorted_sub a lo !mid }
        invariant { permut_sub (at a 'I) a lo (length a) }
        invariant { forall j: int. 0 <= j < lo -> a[j] = (at a 'I)[j] }
        let hi = naturalrec tmp a !mid i in
        assert { permut_sub (at a 'I) a lo (length a) };
        'M:
        merge_using tmp a lo !mid hi;
        assert { permut_sub (at a 'M) a lo hi };
        assert { permut_sub (at a 'M) a lo (length a) };
        mid := hi;
        if !mid = n then raise Break
      done;
      !mid
    with Break -> n end

  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
    ()

320
end