Arrays - Multimedia Introduction to Programming Using Java - page 273

0 i b.length

sorted , ≤ b[i..] ≥ b[0..i - 1] Q2: b

Relation Q2 is like Q1 , but it also requires that everything in the first segment be
at most everything in the second. Q2 is used in algorithm selectionSort , which
is another sorting algorithm.

8.3 Processing array segments

8.3.1 Printing an array segment

We describe how to develop an array-printing algorithm using a relation. We can
print the four values in array segment c[h..h+3] on different lines using four
print statements. However, we cannot print the elements of c[h..k-1] in this
manner because the number of elements is variable, and not a constant. Instead,
we use a loop. To develop the loop, first write a postcondition for the task (this
step is almost always easy):

postcondition R : c[h..k-1] has been printed

To find a loop invariant P , we replace expression k by a fresh variable i :

invariant P : c[h..i-1] has been printed

Here is a diagram for P :

h i k

these have been printed

P: b

How does it start? Since nothing has been printed initially, the invariant is
truthified by making segment c[h..i-1] empty, i.e. by setting i to h .
When is it done? When the invariant and the postcondition are the same.
That happens when i=k . Therefore, the loop should continue as long as i != k .
And we now know the range of i : h≤i≤k .
How does it make progress? i starts at h and moves toward k , so to make
progress toward termination, increment i .
How does it keep the invariant true? By printing c[i] before i is incre-
mented.
Here is the final loop (with initialization):

// Print c[h..k-1]
int i= h;
// inv: h≤i≤k and c[h..i-1] has been printed
while (i != k) {
System.out.println(c[i]);
i= i + 1;

}