Arrays - Multimedia Introduction to Programming Using Java - page 288

0 j b.length

sorted, ≤ b[j..]

P: b

Thus, the elements of the first segment are already in ascending order. Moreover,
they are no larger than those in the second segment. Remember this invariant,
and you can then develop the loop from it whenever necessary, as follows.
The invariant is initially truthified by setting j to 0 , since that makes the first
segment b[0..j-1] empty and makes the second segment b[j..] be the whole
array. Execution of the loop can terminate when j = b.length , since then the
second segment is empty and the first segment is the whole array and is sorted.
Therefore, the loop can continue as long as j != b.length .
Progress is made toward termination by incrementing j . However, this will
maintain the invariant only if b[j] is the minimum value of b[j..] . So, the
repetend consists of statements to make b[j] have this property —see Fig. 8.8.
Note that the procedure is not yet completely in Java, since the assignment
to p has its expression written in English and the swap statement has to be imple-
mented. Nevertheless, if you are explaining selection sort to someone, always
present it in this fashion. We are using abstraction to hide some of the Java code
and bring out the essence of selection sort.
The assignment to p can be rewritten using function min of Sec. 8.4.3. Or,
the function call can be expanded inline, so that the function body would be as
shown in Fig. 8.9. The function body has nested loops. But do not think of them
as nested loops. When studying the outer loop, view its repetend as:

Set p to the index of the min value of b[j..]
Swap b[j] and b[p]

/** Sort b —put its elements in ascending order */
public static void selectionSort( int [] b) {
// inv P: 0 ≤ j ≤ b.length and b[0..j-1] is sorted and b[0..j-1] ≤ b[j..]
for ( int j= 0; j != b.length; j= j + 1) {
// Set p to the index of the minimum value of b[j..]
int p= j; // will contain index of minimum
// inv :j<h≤b.length and b[p] is the minimum of b[j..h-1]
for ( int h= j + 1; h != b.length; h= h + 1) {
if (b[h] < b[p])
{ p= h; }

}
// Swap b[j] and b[p]
int t= b[j]; b[j]= b[p]; b[p]= t; }

}
Figure 8.9:

Function selectionSort