Loops - Multimedia Introduction to Programming Using Java - page 251

A possible loop invariant P can be created by making a copy of postcondition R
and replacing the last integer 2 in it by a fresh variable:
invariant P: 9 , 8 , … , down to k have been printed
How does it start? Initially, nothing has been printed. If k is set to 10 , then the
invariant implies that

9 , 8 , … , down to 10 have been printed
i.e. no numbers have been printed. Therefore, setting k to 10 truthifies P .
When does it stop? Looking at the invariant and the postcondition, we see that
the loop should stop when k is 2 , so it should continue as long as k!=2 .
How does it make progress? By decreasing k .
How does it fix the invariant? By printing the next integer, which is integer k
-1 .

Putting it all together, we get this loop:

// Print 9 , 8 , … , down to 2
// { invariant P: 9 , 8 , … , down to k have been printed }
for ( int k= 10; k != 2; k= k - 1)
{ System.out.println(k - 1); }
// { R: 9 , 8 , … , down to 2 have been printed }

A different invariant, a different loop.
The loop just developed may feel a bit odd: why not start k at 9 , print k , and
stop when k is 1 ? That would work, but it would require a different invariant. A
different invariant P can be created by making a copy of postcondition R and
replacing the last integer 2 in it by k+1 (instead of k ); a self-review exercise in
Sec. 7.5.5 asks you to develop a loop using this invariant.

invariant P: 9 , 8 , … , down to k+1 have been printed

7.5.4 A for-loop schema

Earlier, we presented this schema for processing the first n natural numbers:
// Process natural numbers 0..n-1 , for n≥0
int k= 0;
// { invariant: 0..k-1 have been processed }
while (k != n) {
Process k;
k= k + 1;

Lesson
page 7-4

}
// {0..n-1 have been processed }