(* Sorting an array of integer using quicksort *) (* with partitioning a la Bentley *) module Quicksort use import int.Int use import ref.Ref use import array.Array use import array.IntArraySorted use import array.ArraySwap use import array.ArrayPermut use import array.ArrayEq 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 (* 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 } variant { r - l } = if l + 1 < r then begin let v = a[l] in let m = ref l in 'L: for i = l + 1 to r - 1 do 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 m := !m + 1; swap a i !m; assert { permut_sub (at a 'K) a l r } end done; '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 }; assert { qs_partition (at a 'N) a l !m r v }; 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 *) module Shuffle "Knuth shuffle" use import int.Int use import array.Array use import array.ArraySwap use import array.ArrayPermut use random.Random 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 module QuicksortWithShuffle use import array.Array use import array.IntArraySorted 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 } shuffle a; quicksort a end (* using 3-way partitioning *) module Quicksort3way use import int.Int use import ref.Refint use import array.Array use import array.IntArraySorted 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 } end 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 } shuffle a; quicksort a end module Test use import int.Int use import array.Array use import Quicksort let test1 () = let a = make 3 0 in a[0] <- 7; a[1] <- 3; a[2] <- 1; 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; if a[7] <> 413 then raise BenchFailure; a end