examples/bubble_sort.mlw

   1
   2 (* {1 Bubble sort} *)
   3
   4 module BubbleSort
   5
   6   use int.Int
   7   use ref.Ref
   8   use array.Array
   9   use array.IntArraySorted
  10   use array.ArraySwap
  11   use array.ArrayPermut
  12   use array.ArrayEq
  13
  14   let bubble_sort (a: array int)
  15     ensures { permut_all (old a) a }
  16     ensures { sorted 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] }
  22       for j = 0 to i - 1 do
  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);
  29       done;
  30     done
  31
  32   let test1 () =
  33     let a = make 3 0 in
  34     a[0] <- 7; a[1] <- 3; a[2] <- 1;
  35     bubble_sort a;
  36     a
  37
  38   let test2 () ensures { result.length = 8 } =
  39     let a = make 8 0 in
  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;
  42     bubble_sort a;
  43     a
  44
  45   exception BenchFailure
  46
  47   let bench () raises { BenchFailure -> true } =
  48     let a = test2 () in
  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;
  57     a
  58
  59 end