Java Reference
In-Depth Information
When the loop condition evaluates to
false
,
i=5
. So, when the loop terminates,
the invariant says:
the squares of
2..5-1
have been printed
which means:
the squares of
2..4
have been printed
which is exactly the final assertion!
3. How does it make progress?
We have to be sure that the loop terminates,
which means that at some point the loop condition will become
false
. In this
case,
i
starts out at
2
and ends at
5
. The statement
i= i + 1
; in the repetend
ensures that each iteration makes progress toward the loop condition becoming
false
.
4. How does it fix the invariant?
The invariant must be true each time the loop
condition is evaluated. So, we have to ensure that each execution of the repetend
fixes the variables to keep it
true
. In this case, before the repetend is executed,
we know the following from the loop condition and the loop invariant:
i!=5
and the squares of
2..i-1
have been printed
Therefore, the next value to print is
i*i
. The repetend prints this value and then
increases
i
, after which the invariant again
true
.
The above analysis talked about a particular loop. We now discuss the same
questions with regard to a general loop of this form:
initialization
//
invariant: explains what is true whenever the
condition
is evaluated
while
(
condition
) {
repetend
}
//
postcondition: an assertion of what is supposed to be true at the end
Again, here are the questions we ask when we are understanding a given
loop or writing our own loop:
1. How does it start?
In other words, what
initialization
of variables will make
the invariant true initially? Here are two general strategies for this: try to make a
range empty and set some variable to zero.
2. When does it stop?
When it stops, the invariant is true and the loop condition
is false. From these two facts, we should be able to conclude that the postcondi-
tion is true.
3. How does it make progress?
What statement in the repetend ensures that
after a number of iterations the loop condition will eventually become false?
4. How does it fix the loop invariant?
We have to make sure that the following
precondition-statement-postcondition triple holds:
Search WWH ::
Custom Search