= 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; .
Examples of while-loops
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:
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.