examples/quicksort.mlw

   1
   2 (** {1 Sorting an array of integers using quicksort} *)
   3
   4 (** {2 with a partitioning a la Bentley} *)
   5
   6 module Quicksort
   7
   8   use int.Int
   9   use ref.Ref
  10   use array.Array
  11   use array.IntArraySorted
  12   use array.ArraySwap
  13   use array.ArrayPermut
  14   use array.ArrayEq
  15
  16   predicate qs_partition (a1 a2: array int) (l m r: int) (v: int) =
  17     permut_sub a1 a2 l r /\
  18     (forall j: int. l <= j < m -> a2[j] < v) /\
  19     (forall j: int. m < j < r -> v <= a2[j]) /\
  20     a2[m] = v
  21
  22   (* partitioning à la Bentley, that is
  23
  24      l            i          m          r
  25     +-+----------+----------+----------+
  26     |v|   < v    |    ?     |   >= v   |
  27     +-+----------+----------+----------+     *)
  28
  29   let rec quick_rec (a: array int) (l: int) (r: int) : unit
  30     requires { 0 <= l <= r <= length a }
  31     ensures  { sorted_sub a l r }
  32     ensures  { permut_sub (old a) a l r }
  33     variant  { r - l }
  34   = if l + 1 < r then begin
  35       let v = a[l] in
  36       let m = ref l in
  37       label L in
  38       for i = l + 1 to r - 1 do
  39         invariant { a[l] = v /\ l <= !m < i }
  40         invariant { forall j:int. l < j <= !m -> a[j] < v }
  41         invariant { forall j:int. !m < j <  i -> a[j] >= v }
  42         invariant { permut_sub (a at L) a l r }
  43         label K in
  44         if a[i] < v then begin
  45           m := !m + 1;
  46           swap a i !m;
  47           assert { permut_sub (a at K) a l r }
  48         end
  49       done;
  50       label M in
  51       swap a l !m;
  52       assert { qs_partition (a at M) a l !m r v };
  53       label N in
  54       quick_rec a l !m;
  55       assert { qs_partition (a at N) a l !m r v };
  56       label O in
  57       quick_rec a (!m + 1) r;
  58       assert { qs_partition (a at O) a l !m r v };
  59       assert { qs_partition (a at N) a l !m r v };
  60     end
  61
  62   let quicksort (a: array int) =
  63     ensures { sorted a }
  64     ensures { permut_all (old a) a }
  65     quick_rec a 0 (length a)
  66
  67 end
  68
  69 (** {2 Knuth's shuffle}
  70
  71     A realistic quicksort first shuffles the array. *)
  72
  73 module Shuffle
  74
  75   use int.Int
  76   use array.Array
  77   use array.ArraySwap
  78   use array.ArrayPermut
  79   use random.Random
  80
  81   let shuffle (a: array int) : unit
  82     writes  { a, Random.s }
  83     ensures { permut_all (old a) a }
  84   = for i = 1 to length a - 1 do
  85       invariant { permut_all (old a) a }
  86       swap a i (Random.random_int (i+1))
  87     done
  88
  89 end
  90
  91
  92 module QuicksortWithShuffle
  93
  94   use array.Array
  95   use array.IntArraySorted
  96   use array.ArrayPermut
  97   use Shuffle
  98   use Quicksort
  99
 100   let qs (a: array int) : unit =
 101     ensures { sorted a }
 102     ensures { permut_all (old a) a }
 103     shuffle a;
 104     quicksort a
 105
 106 end
 107
 108 (** {2 with 3-way partitioning}
 109
 110     A realistic quicksort also has to use 3-way partitioning, to cope
 111     with arrays were many values are identical. *)
 112
 113 module Quicksort3way
 114
 115   use int.Int
 116   use ref.Refint
 117   use array.Array
 118   use array.IntArraySorted
 119   use array.ArraySwap
 120   use array.ArrayPermut
 121   use array.ArrayEq
 122
 123   predicate qs_partition (a1 a2: array int) (l ml mr r: int) (v: int) =
 124     permut_sub a1 a2 l r /\
 125     (forall j: int. l  <= j < ml -> a2[j] < v) /\
 126     (forall j: int. ml <= j < mr -> a2[j] = v) /\
 127     (forall j: int. mr <= j < r  -> a2[j] > v)
 128
 129   (* 3-way partitioning
 130
 131      l          ml         i          mr          r
 132     +----------+----------+----------+-----------+
 133     |   < v    |    = v   |     ?    |    > v    |
 134     +----------+----------+----------+-----------+       *)
 135
 136   let rec quick_rec (a: array int) (l r: int) : unit
 137     requires { 0 <= l <= r <= length a }
 138     ensures  { sorted_sub a l r }
 139     ensures  { permut_sub (old a) a l r }
 140     variant  { r - l }
 141   = if l + 1 < r then begin
 142       let v  = a[l] in
 143       let ml = ref l in
 144       let mr = ref r in
 145       let i  = ref (l + 1) in
 146       label L in
 147       while !i < !mr do
 148         invariant { l <= !ml < !i <= !mr <= r }
 149         invariant { forall j: int. l   <= j < !ml -> a[j] < v }
 150         invariant { forall j: int. !ml <= j < !i  -> a[j] = v }
 151         invariant { forall j: int. !mr <= j < r   -> a[j] > v }
 152         invariant { permut_sub (a at L) a l r }
 153         variant   { !mr - !i }
 154         label K in
 155         if a[!i] < v then begin
 156           swap a !ml !i;
 157           incr ml;
 158           incr i;
 159           assert { permut_sub (a at K) a l r }
 160         end else if a[!i] > v then begin
 161           decr mr;
 162           swap a !i !mr;
 163           assert { permut_sub (a at K) a l r }
 164         end else
 165           incr i
 166       done;
 167       assert { qs_partition (a at L) a l !ml !mr r v };
 168       label N in
 169       quick_rec a l !ml;
 170       assert { qs_partition (a at N) a l !ml !mr r v };
 171       label O in
 172       quick_rec a !mr r;
 173       assert { qs_partition (a at O) a l !ml !mr r v };
 174       assert { qs_partition (a at N) a l !ml !mr r v }
 175     end
 176
 177   let quicksort (a: array int) =
 178     ensures { sorted a }
 179     ensures { permut_all (old a) a }
 180     quick_rec a 0 (length a)
 181
 182   use Shuffle
 183
 184   let qs (a: array int) : unit =
 185     ensures { sorted a }
 186     ensures { permut_all (old a) a }
 187     shuffle a;
 188     quicksort a
 189
 190 end
 191
 192 module Test
 193
 194   use int.Int
 195   use array.Array
 196   use Quicksort
 197
 198   let test1 () =
 199     let a = make 3 0 in
 200     a[0] <- 7; a[1] <- 3; a[2] <- 1;
 201     quicksort a;
 202     a
 203
 204   let test2 () ensures { result.length = 8 } =
 205     let a = make 8 0 in
 206     a[0] <- 53; a[1] <- 91; a[2] <- 17; a[3] <- -5;
 207     a[4] <- 413; a[5] <- 42; a[6] <- 69; a[7] <- 6;
 208     quicksort a;
 209     a
 210
 211   exception BenchFailure
 212
 213   let bench () raises { BenchFailure -> true } =
 214     let a = test2 () in
 215     if a[0] <> -5 then raise BenchFailure;
 216     if a[1] <> 6 then raise BenchFailure;
 217     if a[2] <> 17 then raise BenchFailure;
 218     if a[3] <> 42 then raise BenchFailure;
 219     if a[4] <> 53 then raise BenchFailure;
 220     if a[5] <> 69 then raise BenchFailure;
 221     if a[6] <> 91 then raise BenchFailure;
 222     if a[7] <> 413 then raise BenchFailure;
 223     a
 224
 225 end
 226
 227 module Traditional
 228
 229   use int.Int
 230   use ref.Refint
 231   use array.Array
 232   use array.IntArraySorted
 233   use array.ArraySwap
 234   use array.ArrayPermut
 235   use array.ArrayEq
 236
 237   let rec quick_rec (a: array int) (l: int) (r: int) : unit
 238     requires { 0 <= l <= r <= length a }
 239     ensures  { sorted_sub a l r }
 240     ensures  { permut_sub (old a) a l r }
 241     variant  { r - l }
 242   = if l + 1 >= r then return;
 243     let v = a[l] in
 244     let ref i = l in
 245     let ref j = r in
 246     while true do
 247       invariant { l <= i < r-1 }
 248       invariant { forall k. l <= k <= i -> a[k] <= v }
 249       invariant { l < j <= r }
 250       invariant { forall k. j <= k < r -> a[k] >= v }
 251       invariant { permut_sub (old a) a l r }
 252       invariant { a[l] = v }
 253       variant   { j - i }
 254       label L in
 255       (* while (a[++i] < v) { if (i == r-1) break; } *)
 256       incr i;
 257       while a[i] < v do
 258         invariant { i at L < i < r }
 259         invariant { forall k. l <= k < i -> a[k] <= v }
 260         variant   { r - i }
 261         if i = r - 1 then break;
 262         incr i
 263       done;
 264       (* while (v < a[--j]) { if (j == l) break; } *)
 265       decr j;
 266       while a[j] > v do
 267         invariant { l <= j < j at L }
 268         invariant { forall k. j < k < r -> a[k] >= v }
 269         variant { j }
 270         if j = l then break;
 271         decr j;
 272       done;
 273       if i >= j then break;
 274       swap a i j
 275     done;
 276     swap a l j;
 277     quick_rec a l     j;
 278     quick_rec a (j+1) r
 279
 280   let quicksort (a: array int) : unit
 281     ensures { sorted a }
 282     ensures { permut_all (old a) a }
 283   = (* insert a call to shuffle here if you wish *)
 284     quick_rec a 0 (length a)
 285
 286 end