Arrays - Multimedia Introduction to Programming Using Java - page 274

Because this loops over a range, a for -loop could have been used instead:
// Print c[h..k-1]
// inv: h≤i≤k and c[h..i-1] has been printed
for ( int i = h; i != k; i= i + 1) {
System.out.println(c[i]);

}

8.3.2 A schema to process arrays

We step back from the loop above and make it more abstract, as shown below.
First, instead of printing each array element, we say to “process it”. Next, the
invariant indicates what has been processed instead of what has been printed.
Most of the loop remains the same! Only the repetend is changed, into an English
statement to process element c[i] .
// Process elements of c[h..k-1] , in order
// inv: h ≤ i ≤ k and c[h..i-1] has been processed
for ( int i= h; i != k; i= i + 1) {
Process c[i]

See lesson 8.3
to get these
schemas from
ProgramLive .

}
Whenever you have to process an array segment, you can use this schema
rather than develop the loop from scratch.

8.3.3 A schema to process in reverse

We develop a program schema to process the elements of array segment
c[h..k-1] , but in reverse order. First we write a postcondition:
postcondition: c[h..k-1] has been processed in reverse order
Now we find a loop invariant P . Since the elements are to be processed from
the end to the beginning, we replace expression h by a fresh variable i :
invariant P : c[i..k-1] has been processed in reverse order
We now develop a for -loop.
How does it start ? Because nothing has been processed initially, we truthify
the invariant by setting i to k , making segment c[i..k-1] empty.
When is it done ? Given the invariant, the postcondition is true when i=h .
Therefore, the loop should continue as long as i differs from h . And we now
know the range of i : h≤i≤k .
How does it make progress ? Variable i starts at k and moves toward h , so to
make progress toward termination, decrement i .
How does it keep the invariant true ? From the loop invariant, we see that
array element c[i - 1] should be processed.

Activity
8-3.2