mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
107 lines
2.9 KiB
Plaintext
107 lines
2.9 KiB
Plaintext
|
|
(* {1 Bubble sort} *)
|
|
|
|
module BubbleSort
|
|
|
|
use int.Int
|
|
use ref.Ref
|
|
use array.Array
|
|
use array.IntArraySorted
|
|
use array.ArraySwap
|
|
use array.ArrayPermut
|
|
|
|
let bubble_sort (a: array int)
|
|
ensures { permut_all (old a) a }
|
|
ensures { sorted a }
|
|
= for i = length a - 1 downto 1 do
|
|
invariant { permut_all (old a) a }
|
|
invariant { sorted_sub a i (length a) }
|
|
invariant { forall k1 k2: int.
|
|
0 <= k1 <= i < k2 < length a -> a[k1] <= a[k2] }
|
|
for j = 0 to i - 1 do
|
|
invariant { permut_all (old a) a }
|
|
invariant { sorted_sub a i (length a) }
|
|
invariant { forall k1 k2: int.
|
|
0 <= k1 <= i < k2 < length a -> a[k1] <= a[k2] }
|
|
invariant { forall k. 0 <= k <= j -> a[k] <= a[j] }
|
|
if a[j] > a[j+1] then swap a j (j+1);
|
|
done;
|
|
done
|
|
|
|
let test1 () =
|
|
let a = make 3 0 in
|
|
a[0] <- 7; a[1] <- 3; a[2] <- 1;
|
|
bubble_sort 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;
|
|
bubble_sort 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
|
|
|
|
(* {2 Knuth's version}
|
|
|
|
This is the version of bubble sort we can find in TAOCP, volume 3,
|
|
section 5.2.2 (page 107).
|
|
|
|
Though Knuth is concluding with ``In short, the bubble sort seems
|
|
to have nothing to recommend it, except a catchy name and the fact
|
|
that it leads to some interesting theoretical problems'', the
|
|
following makes yet another nice exercise in program verification.
|
|
|
|
*)
|
|
|
|
module TAOCP
|
|
|
|
use int.Int
|
|
use ref.Ref
|
|
use array.Array
|
|
use array.IntArraySorted
|
|
use array.ArraySwap
|
|
use array.ArrayPermut
|
|
|
|
let bubble_sort (a: array int) : unit
|
|
writes { a }
|
|
ensures { permut_all (old a) a }
|
|
ensures { sorted a }
|
|
= let n = length a in
|
|
let ref bound = n in
|
|
while bound >= 2 do
|
|
invariant { bound <= n }
|
|
invariant { permut_all (old a) a }
|
|
invariant { forall i1 i2. 0 <= i1 < bound <= i2 < n -> a[i1] <= a[i2] }
|
|
invariant { sorted_sub a bound n }
|
|
variant { bound }
|
|
let ref t = 0 in
|
|
for j = 0 to bound - 2 do
|
|
invariant { 0 <= t <= j }
|
|
invariant { permut_all (old a) a }
|
|
invariant { forall i1 i2. 0 <= i1 < bound <= i2 < n -> a[i1] <= a[i2] }
|
|
invariant { forall i. 0 <= i <= t -> a[i] <= a[t] }
|
|
invariant { sorted_sub a t (j+1) }
|
|
invariant { sorted_sub a bound n }
|
|
if a[j] > a[j+1] then (swap a j (j+1); t <- j+1)
|
|
done;
|
|
bound <- t
|
|
done
|
|
|
|
end
|