Loops - Multimedia Introduction to Programming Using Java - page 252

This loop has a loop counter, so we can also present it as the following for-
loop schema. This schema is used often for developing loops.

// Process natural numbers 0..n-1 , for n≥0
// { invariant: 0..k-1 have been processed }
for ( int k= 0; k != n; k= k + 1) {
Process k;

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

7.5.5 Self-review exercises

SR1 . Write another solution to the problem in Sec. 7.5.3, but this time use this
postcondition and invariant when you answer the four loopy questions:

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

Answers to self review exercises

SR1. How does it start? Initially, nothing has been printed. If we set k to 9 , then
the invariant has the meaning:

9 , 8 , … , down to 10 have been printed
which means that no numbers have been printed.

When does it stop? Looking at the invariant and the postcondition, we see that
the loop should stop when k is 1 , so it should continue as long as k!=1 .
How does it make progress? By decreasing k .
How does it fix the invariant? By printing the next integer, which is integer k .

7.6 Making progress and stopping

7.6.1 Why use condition i != n?

Suppose we have a loop like this one:

Activity
7-5.2

int i= 0;
// { invariant: … }
while (i != n) {
Process i;
i= i + 1;

}