why3/examples/selection_sort.mlw

(* Selection sort. *)

module SelectionSort

  use int.Int
  use ref.Ref
  use array.Array
  use array.IntArraySorted
  use array.ArraySwap
  use array.ArrayPermut
  use array.ArrayEq

  let selection_sort (a: array int)
    ensures { sorted a /\ permut_all (old a) a } =
    let min = ref 0 in
    for i = 0 to length a - 1 do
      (* a[0..i[ is sorted; now find minimum of a[i..n[ *)
      invariant { sorted_sub a 0 i /\ permut_all (old a) a /\
          forall k1 k2: int. 0 <= k1 < i <= k2 < length a -> a[k1] <= a[k2] }
      (* let min = ref i in *) min := i;
      for j = i + 1 to length a - 1 do
        invariant {
          i <= !min < j && forall k: int. i <= k < j -> a[!min] <= a[k] }
        if a[j] < a[!min] then min := j
      done;
      label L in
      if !min <> i then swap a !min i;
      assert { permut_all (a at L) a }
    done

  let test1 () =
    let a = make 3 0 in
    a[0] <- 7; a[1] <- 3; a[2] <- 1;
    selection_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;
    selection_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