Java Reference
In-Depth Information
invariant: roach population after w weeks is population and
week w- 1's roach volume < apartmentVolume
The postcondition and the invariant differ only in that the postcondition has
one more piece: the roach volume has exceeded the apartment volume.
We now develop the loop using our methodology.
How does it start? The roach population after 0 weeks is 100 . So, we use
the assignments:
w= 0;
population= 100;
When does it stop? When the roach volume is big enough: the roach vol-
ume ≥ apartmentVolume . So the loop condition is the complement of this rela-
tion. Remember, the roach volume is the product of a single-roach volume and
the number of roaches.
How does it make progress? The postcondition requires that apartment-
Volume ≤ roach volume. In order to make progress toward this, the number of
roaches has to increase. According to the roach-population-growth rule at the
beginning of this section, this means adding population * 1.25 to population
(because the population increases by 125 percent). Here, we do the equivalent:
multiply by 5 and divide by 4 , so that all the operations are of type int .
How does it fix the invariant? Because the roach population grows week-
ly, the week number increases by 1.
/* Calculate the number w of weeks it takes a roach infestation to
completely fill an apartment */
int w= 0;
int population= 100; // roach population after w weeks
/* invariant: roach population after w weeks is population and
week w-1 's roach volume < apartmentVolume */
while (apartmentVolume > population * .001) {
population= population + (5 * population) / 4;
w= w + 1;
See lesson
page 7-2 to ob-
tain this loop
Figures. 7.1a and 7.1b contain two loops that compute the value b c ( b multiplied
by itself c times) where b and c are int s. For example, 2 3 = 2 * 2 * 2=8 ; and
2 0 = 1 . We use the second loop to illustrate the power of loop invariants because
it is very hard to understood and develop without an invariant, and it is a much
faster algorithm for computing an exponent.
The straightforward approach
In the first loop, y is the remaining number of times to multiply by b . Each
Search WWH ::

Custom Search