Loops - Multimedia Introduction to Programming Using Java - page 244

Process 0;
Process 1;
…
Process n-1;
We can easily write down a postcondition for the loop:

See lesson page
7-3 to obtain
the schema.

0..n-1 have been processed
To develop a loop invariant, we make a copy of the postcondition and replace n
in it by a fresh variable k :
invariant: 0..k-1 have been processed
How does it start? The invariant has the nice property that assigning 0 to k
truthifies it, because the invariant then means that no natural numbers have been
processed.
When does it stop? The loop should stop when k=n because then the
invariant implies that the postcondition is true. So, the loop should continue as
long as k!=n .
How does it make progress? Variable k starts out at 0 and is supposed to
end up at n , so to make progress, increment k .
How does it fix the invariant? Since k is being incremented, the next num-
ber must be processed. The invariant tells us that the next number is k .
This leads to the loop schema of Fig. 7.2.

7.4.2 A loop to count the w's

We write a loop to count the number of w 's in a string s , starting with the schema
of Fig. 7.2. We can use this schema because the task is to process the characters
of s , and these have numbers in the range 0..s.length()-1 , so we are really
processing the integers in this range.
The first step is to rewrite the schema in the context of our problem. We
begin by replacing n in the schema by s.length() .

Activity
7-3.2

// Process the n 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;

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

Figure 7.2: A schema to process natural numbers 0..n-1