@pre  0 <= |a| &&  0 <= l && l < |a|  &&
             -1 <= u  && u < |a|
@post |rv| = |a| && (0 = |a| -> sorted(rv, 0, 0)) ||
      (0 < |a| -> sorted(rv, 0, l))

int[] swapMin(int[] a, int l, int u) {
    int min;
    int[] array := a;

    min := array[l];

    for
    @ P : 0<=l && i > l && |a|=|array| && u>=-1 && i<=u+1
    # (u-i+2)
    (int i := l + 1; i <= u; i := i + 1) {

        if (array[i] < min) {
          min := array[i];
          array[i] := array[l];
          array[l] := min;
        }
    }
    return array;
}

@pre  |a|>=0
@post (0 = |a| -> sorted(rv, 0, 0)) ||
      (0 < |a| -> sorted(rv, 0, |a| - 1))
int[] selectSort(int[] a) {
    int minIndex;
    int t;

    int[] array := a;

    for
    @T: i >= 0 && 0 <= |array| && i<= |array|+1
    # (|array|-i+1)
    (int i := 0; i < |array| ; i := i + 1) {
        array := swapMin(array, i, |array| - 1);
    }

    return array;
}