9 use array.IntArraySorted
14 let bubble_sort (a: array int)
15 ensures { permut_all (old a) a }
17 = for i = length a - 1 downto 1 do
18 invariant { permut_all (old a) a }
19 invariant { sorted_sub a i (length a) }
20 invariant { forall k1 k2: int.
21 0 <= k1 <= i < k2 < length a -> a[k1] <= a[k2] }
23 invariant { permut_all (old a) a }
24 invariant { sorted_sub a i (length a) }
25 invariant { forall k1 k2: int.
26 0 <= k1 <= i < k2 < length a -> a[k1] <= a[k2] }
27 invariant { forall k. 0 <= k <= j -> a[k] <= a[j] }
28 if a[j] > a[j+1] then swap a j (j+1);
34 a[0] <- 7; a[1] <- 3; a[2] <- 1;
38 let test2 () ensures { result.length = 8 } =
40 a[0] <- 53; a[1] <- 91; a[2] <- 17; a[3] <- -5;
41 a[4] <- 413; a[5] <- 42; a[6] <- 69; a[7] <- 6;
45 exception BenchFailure
47 let bench () raises { BenchFailure -> true } =
49 if a[0] <> -5 then raise BenchFailure;
50 if a[1] <> 6 then raise BenchFailure;
51 if a[2] <> 17 then raise BenchFailure;
52 if a[3] <> 42 then raise BenchFailure;
53 if a[4] <> 53 then raise BenchFailure;
54 if a[5] <> 69 then raise BenchFailure;
55 if a[6] <> 91 then raise BenchFailure;
56 if a[7] <> 413 then raise BenchFailure;