Java Reference
In-Depth Information
In this version,
c
is not mentioned in the invariant, so why is it set to
0
in two
places? What purpose does it serve? What meaning would you give
c
if it were
to be mentioned in the invariant? Variable
c
has no place in the program, and it
should be deleted. There is absolutely no reason for it being in there.
After removing c and then implementing the statement:
Process pairs
(r, 0), …, (r, C - 1)
we wind up with the program segment of Fig. 7.8. There is a variable c, but it is
local to the implementation of the above statement.
We now have a well-designed program segment.
7.8
Key concepts
•
Loop
. A
repetitive statement
, or
iterative statement
, or
loop
is a statement that
calls for the repeated execution of its
repetend
.
•
While-loop
. The
while-loop
has the form:
while
(
condition
)
repetend
.
•
For-loop
. The
for-loop
has the form:
for
(
initialization
;
condition
;
progress
)
repetend
. It can be viewed as an abbreviation of a while-loop that has a
loop
counter
.
•
Loop invariant
. A
loop invariant
is a relation that is true before and after each
loop iteration. A loop is understood in terms of the loop invariant by answering
four loopy questions:
1.
How does it start?
What assignments make the invariant true
initially?
2.
When does it stop?
The invariant, together with the falsity of
the loop condition, has to imply that the postcondition is true.
3.
How does it make progress?
Execution of the repetend has to
ensure that after a finite number of iterations the loop terminates.
4.
How does it fix the loop invariant?
Each execution of the
repetend begins with the invariant true, and it must end with it
true as well.
•
Nested loops
. Abstraction should be used to hide nested loops: use a statement-
comment that says what the repetend does, which can be used to understand the
outer loop without thinking in terms of nested loops.
Exercises for Chapter 7
Many of these exercises ask you to write a loop (with initialization), given the
task to be performed, a postcondition, and loop invariant. Develop the loop using
Search WWH ::
Custom Search