Java Reference

In-Depth Information

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) }

Search WWH ::

Custom Search