Selection sort as in Sedgewick

Fully automatic

with use of swap

without swap, one should add assert{ permut a (a at 'L1) } (L1 at end of inner loop)

module SelectionSort

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

  let swap (a: array int) (i: int) (j: int) =
    requires { 0 <= i < length a /\ 0 <= j < length a }
    ensures { exchange (old a) a i j }
   let v = a[i] in
    a[i] <- a[j];
    a[j] <- v

  let selection_sort (a: array int) =
    ensures { permut_all (old a) a }
'L:
    for i = 0 to length a - 1 do
      invariant { permut_all (at a 'L) a }
      let min = ref i in
      for j = i + 1 to length a - 1 do
        invariant { i <= !min < j }
        if a[j] < a[!min] then min := j
      done;
      if !min <> i then swap a !min i
    done

end