quicksort: shuffle is implemented *and used*

parent ddbfb32a
......@@ -63,14 +63,22 @@ end
(* a realistic quicksort first shuffles the array *)
module Shuffle
module Shuffle "Knuth shuffle"
use import int.Int
use import array.Array
use import array.ArraySwap
use import array.ArrayPermut
use random.Random
val shuffle (a: array int) : unit
writes { a }
let shuffle (a: array int) : unit
writes { a, Random.s }
ensures { permut_all (old a) a }
= '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
end
......@@ -86,6 +94,7 @@ module QuicksortWithShuffle
let qs (a: array int) : unit =
ensures { sorted a }
ensures { permut_all (old a) a }
shuffle a;
quicksort a
end
......@@ -162,6 +171,7 @@ module Quicksort3way
let qs (a: array int) : unit =
ensures { sorted a }
ensures { permut_all (old a) a }
shuffle a;
quicksort a
end
......
This diff is collapsed.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment