Loops - Multimedia Introduction to Programming Using Java - page 246

The first time one sees the development of a loop from a schema, it seems
like a lot of extra work. However, with practice, it becomes second nature to
think in terms of the schema, rather than develop a loop from scratch all the time,
and the whole process becomes easier and more efficient. Develop a few loops
this way, and you will get to the point where you can do it without even having
to look at the schema.

7.4.3 Testing primality

We use the schema of Fig. 7.2 again, but this time with slight variations on the
theme. We write a loop, with initialization, to determine whether variable p is
prime. Recall that a prime is an integer that is greater than 1 and whose only pos-
itive divisors are 1 and itself. The result is stored in variable b : upon termination
b is true if and only if p is a prime.
We can use this schema because our task requires processing a range of nat-
ural numbers. The range starts at 2 and ends at p-1 , so we change the schema
accordingly, to start processing at 2 instead of 0 . And we replace n by p .
// Process natural numbers 2..p-1
int k= 2;
// { invariant: 2..k-1 have been processed }
while (k != p) {
Process k;
k= k + 1;

Activity
7-3.3

}
// {2.( -1 have been processed }
Our concrete postcondition is the following:

postcondition: b==(p>1 and no integer in 2..p-1 divides p)
The invariant of the schema is the same as the postcondition of the schema
except that it has k in the range instead of p . Quite likely, the concrete invariant
will bear the same relationship to the concrete postcondition:

invariant: b==(p>1 and no integer in 2..k-1 divides p)
Therefore, we have this algorithm:

See lesson
page 7-3 to ob-
tain the loop

int k= 2;
// Assign to p to truthify the invariant ;
// { inv: b==(p>1 and no integer in 2..k-1 divides p) }
while (k != p) {
Process k;
k= k + 1;

}
// { b==(p>1 and no integer in 2..p-1 divides p) }