@pre true @post true int[] swapMin(int[] a, int l, int u) { int min; int[] array := a; min := array[l]; for @ true (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 true @post sorted(rv, 0, |a| - 1) int[] selectSort(int[] a) { int minIndex; int t; int[] array := a; for @ true (int i := 0; i < |array| ; i := i + 1) { array := swapMin(array, i, |array| - 1); } return array; }