quicksort.mlw 5.55 KB
Newer Older
1

2
(* Sorting an array of integer using quicksort *)
3

4
(* with partitioning a la Bentley *)
5

6 7 8
module Quicksort

  use import int.Int
9 10
  use import ref.Ref
  use import array.Array
11
  use import array.IntArraySorted
12
  use import array.ArraySwap
13 14 15
  use import array.ArrayPermut
  use import array.ArrayEq

16 17 18 19 20
  predicate qs_partition (a1 a2: array int) (l m r: int) (v: int) =
    permut_sub a1 a2 l r /\
    (forall j: int. l <= j < m -> a2[j] < v) /\
    (forall j: int. m < j < r -> v <= a2[j]) /\
    a2[m] = v
21

22 23 24 25 26 27 28 29 30 31 32
  (* partitioning à la Bentley, that is

     l            i          m          r
    +-+----------+----------+----------+
    |v|   < v    |    ?     |   >= v   |
    +-+----------+----------+----------+     *)

  let rec quick_rec (a: array int) (l: int) (r: int) : unit
    requires { 0 <= l <= r <= length a }
    ensures  { sorted_sub a l r }
    ensures  { permut_sub (old a) a l r }
33 34
    variant  { r - l }
  = if l + 1 < r then begin
35
      let v = a[l] in
36
      let m = ref l in
37
  'L: for i = l + 1 to r - 1 do
38 39 40 41 42
        invariant { a[l] = v /\ l <= !m < i }
        invariant { forall j:int. l < j <= !m -> a[j] < v }
        invariant { forall j:int. !m < j <  i -> a[j] >= v }
        invariant { permut_sub (at a 'L) a l r }
    'K: if a[i] < v then begin
43
          m := !m + 1;
44 45
          swap a i !m;
          assert { permut_sub (at a 'K) a l r }
46
        end
47
      done;
48 49 50 51 52 53
  'M: swap a l !m;
      assert { qs_partition (at a 'M) a l !m r v };
  'N: quick_rec a l !m;
      assert { qs_partition (at a 'N) a l !m r v };
  'O: quick_rec a (!m + 1) r;
      assert { qs_partition (at a 'O) a l !m r v };
54
      assert { qs_partition (at a 'N) a l !m r v };
55 56 57 58 59 60 61 62 63 64 65
    end

  let quicksort (a: array int) =
    ensures { sorted a }
    ensures { permut_all (old a) a }
    quick_rec a 0 (length a)

end

(* a realistic quicksort first shuffles the array *)

66
module Shuffle "Knuth shuffle"
67

68
  use import int.Int
69
  use import array.Array
70
  use import array.ArraySwap
71
  use import array.ArrayPermut
72
  use random.Random
73

74 75
  let shuffle (a: array int) : unit
    writes  { a, Random.s }
76
    ensures { permut_all (old a) a }
77 78 79 80 81
  = 'L:
    for i = 1 to length a - 1 do
      invariant { permut_all (at a 'L) a }
      swap a i (Random.random_int (i+1))
    done
82 83 84 85 86 87 88

end


module QuicksortWithShuffle

  use import array.Array
89
  use import array.IntArraySorted
90 91 92 93 94 95 96
  use import array.ArrayPermut
  use import Shuffle
  use import Quicksort

  let qs (a: array int) : unit =
    ensures { sorted a }
    ensures { permut_all (old a) a }
97
    shuffle a;
98 99 100 101 102 103 104 105 106 107 108
    quicksort a

end

(* using 3-way partitioning *)

module Quicksort3way

  use import int.Int
  use import ref.Refint
  use import array.Array
109
  use import array.IntArraySorted
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
  use import array.ArraySwap
  use import array.ArrayPermut
  use import array.ArrayEq

  predicate qs_partition (a1 a2: array int) (l ml mr r: int) (v: int) =
    permut_sub a1 a2 l r /\
    (forall j: int. l  <= j < ml -> a2[j] < v) /\
    (forall j: int. ml <= j < mr -> a2[j] = v) /\
    (forall j: int. mr <= j < r  -> a2[j] > v)

  (* 3-way partitioning

     l          ml         i          mr          r
    +----------+----------+----------+-----------+
    |   < v    |    = v   |     ?    |    > v    |
    +----------+----------+----------+-----------+       *)

  let rec quick_rec (a: array int) (l r: int) : unit
    requires { 0 <= l <= r <= length a }
    ensures  { sorted_sub a l r }
    ensures  { permut_sub (old a) a l r }
    variant  { r - l }
  = if l + 1 < r then begin
      let v  = a[l] in
      let ml = ref l in
      let mr = ref r in
      let i  = ref (l + 1) in
  'L: while !i < !mr do
        invariant { l <= !ml < !i <= !mr <= r }
        invariant { forall j: int. l   <= j < !ml -> a[j] < v }
        invariant { forall j: int. !ml <= j < !i  -> a[j] = v }
        invariant { forall j: int. !mr <= j < r   -> a[j] > v }
        invariant { permut_sub (at a 'L) a l r }
        variant   { !mr - !i }
    'K: if a[!i] < v then begin
          swap a !ml !i;
          incr ml;
          incr i;
          assert { permut_sub (at a 'K) a l r }
        end else if a[!i] > v then begin
          decr mr;
          swap a !i !mr;
          assert { permut_sub (at a 'K) a l r }
        end else
          incr i
      done;
      assert { qs_partition (at a 'L) a l !ml !mr r v };
  'N: quick_rec a l !ml;
      assert { qs_partition (at a 'N) a l !ml !mr r v };
  'O: quick_rec a !mr r;
      assert { qs_partition (at a 'O) a l !ml !mr r v };
      assert { qs_partition (at a 'N) a l !ml !mr r v }
162
    end
163

164 165 166 167 168 169 170 171 172 173
  let quicksort (a: array int) =
    ensures { sorted a }
    ensures { permut_all (old a) a }
    quick_rec a 0 (length a)

  use import Shuffle

  let qs (a: array int) : unit =
    ensures { sorted a }
    ensures { permut_all (old a) a }
174
    shuffle a;
175
    quicksort a
176

177 178 179 180 181 182 183
end

module Test

  use import int.Int
  use import array.Array
  use import Quicksort
184 185 186

  let test1 () =
    let a = make 3 0 in
187
    a[0] <- 7; a[1] <- 3; a[2] <- 1;
188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208
    quicksort a;
    a

  let test2 () ensures { result.length = 8 } =
    let a = make 8 0 in
    a[0] <- 53; a[1] <- 91; a[2] <- 17; a[3] <- -5;
    a[4] <- 413; a[5] <- 42; a[6] <- 69; a[7] <- 6;
    quicksort a;
    a

  exception BenchFailure

  let bench () raises { BenchFailure -> true } =
    let a = test2 () in
    if a[0] <> -5 then raise BenchFailure;
    if a[1] <> 6 then raise BenchFailure;
    if a[2] <> 17 then raise BenchFailure;
    if a[3] <> 42 then raise BenchFailure;
    if a[4] <> 53 then raise BenchFailure;
    if a[5] <> 69 then raise BenchFailure;
    if a[6] <> 91 then raise BenchFailure;
209 210
    if a[7] <> 413 then raise BenchFailure;
    a
211

212
end