Java Reference
In-Depth Information
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.
Processing array segments
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-
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) {
i= i + 1;
Search WWH ::

Custom Search