bubble_sort.mlw 1.56 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1 2 3 4 5

(* {1 Bubble sort} *)

module BubbleSort

6 7 8 9 10 11 12
  use int.Int
  use ref.Ref
  use array.Array
  use array.IntArraySorted
  use array.ArraySwap
  use array.ArrayPermut
  use array.ArrayEq
MARCHE Claude's avatar
MARCHE Claude committed
13 14

  let bubble_sort (a: array int)
15
    ensures { permut_all (old a) a }
MARCHE Claude's avatar
MARCHE Claude committed
16
    ensures { sorted a }
17
  = for i = length a - 1 downto 1 do
18
      invariant { permut_all (old a) a }
MARCHE Claude's avatar
MARCHE Claude committed
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] }
MARCHE Claude's avatar
MARCHE Claude committed
22
      for j = 0 to i - 1 do
23
        invariant { permut_all (old a) a }
MARCHE Claude's avatar
MARCHE Claude committed
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] }
MARCHE Claude's avatar
MARCHE Claude committed
27 28 29 30 31 32 33
        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
34
    a[0] <- 7; a[1] <- 3; a[2] <- 1;
MARCHE Claude's avatar
MARCHE Claude committed
35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59
    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