Java Reference

In-Depth Information

=
1
, (h)
h=1
, (i)
k=n
, (j)
z=0
, (k)
x*y
=
0
(or
x=0||y=0
), (l)
h=1
.

SR3.
(a)
h= h + 1;
, (b)
h= h - 1;
, (c)
h= h - 1
; (d)
h= h + 1
;

SR4.
(a)
s= s + (h + 1);
(b)
s= s + h;
(c)
s= s + (k - 1);
, (d)
s= s + k;
, (e)

s= s - h;
, (f)
z= z + x;
, (g)
x= x + x;
.

7.3

Examples of while-loops

7.3.1

The roach explosion

Your new apartment is infested with roaches, and they are multiplying rapidly.

You would like to figure out how long it will take for them to completely fill up

the apartment. You have measured the nasty things and have determined that they

average
.001
cubic feet each —they are big! While measuring, you found out

that there were about
100
of them to start. You have been told that, if unchecked,

the population more than doubles every week, increasing by
125
percent. You are

going to write a program segment to figure out how many weeks it will take for

them to completely fill the apartment.

The basic idea of a program is straightforward: calculate how many roaches

there are after weeks
1
,
2
,
3
, and so on, and stop as soon as the volume of the

roaches is at least the volume of the apartment. This requires a loop, and we

begin its development by figuring out its postcondition.

We assume that the volume of the apartment is in variable
apartment-

Volume
. We need a variable
w
to contain the number of weeks and another vari-

able
population
to contain the population at the end of
w
weeks:

the roach population after
w
weeks is
population

This property of
w
and
population
will hold when the program segment ter-

minates. But there is more to say about what is true upon termination. First, the

apartment volume is at most the roach volume because termination occurs when

there are enough roaches to fill the apartment. Second, the roaches filled the

apartment only in week
w
because the loop did not terminate in week
w-1
. Thus,

we have this postcondition:

Activity

7-2.2

postcondition: the roach population after
w
weeks is
population
, and

apartmentVolume ≤
roach volume, and

week
w-1
's roach volume
< apartmentVolume

Developing the loop invariant

We now think about the loop invariant. The property of
population
and
w

should remain true and thus should be part of the invariant. The second part of

the postcondition cannot be part of the invariant —that is the difficult part to cal-

culate; that is what the loop is for. However, the third part will be true initially,

when there are very few roaches. Since it is expected to be true initially and true

at the end, we make sure it is always true by placing it in the loop invariant.

Search WWH ::

Custom Search