Java Reference
In-Depth Information
// { the squares of 2..1 have been printed }
System.out.println(2 * 2);
// { the squares of 2..2 have been printed }
System.out.println(3 * 3);
// { the squares of 2..3 have been printed }
System.out.println(4 * 4);
// { the squares of 2..4 have been printed }
Each assertion explains exactly what has been printed at that point in exe-
cution. Note the use of the range 2..1 in the first assertion to say that no squares
have been printed. This notation allows us to write all four assertions in the same
form, which, as you will see, is important when finding a good loop comment.
We want to place the same kind of information in the while-loop, but, since
there is only one println statement in the repetend, we cannot insert all four
assertions in the statement sequence! But note that the assertions are exactly the
same except for the last value of the range. Thus, each assertion has the form
shown below, but each has a different value in place of variable i :
loop assertion : the squares of 2..i-1 have been printed
We call this loop assertion an invariant of the loop because it remains invari-
antly true throughout execution ( invariant means non-changing ). We can think
of this relation as a generalization of the four assertions in the sequence: the
range in the assertion increases with i . Below, we have placed this invariant as a
comment between the initialization and the loop:
// Print the squares of integers in the range 2..4
int i= 2;
// { invariant: the squares of 2..i-1 have been printed }
while (i != 5) {
System.out.println(i * i);
i= i + 1;
}
// { the squares of 2..4 have been printed }
We now look at how we understand a loop that is annotated with such an
invariant. We ask ourselves four questions:
1. How does it start? This question involves the initialization. Why is variable
i initialized to 2 ? Answer: because that initialization truthifies the invariant
before any real work is done.
2. When is it done? When the loop terminates, the last assertion had better be
true. In our running example, at the end, the squares of values in the range 2..4
have been printed. The invariant says this:
invariant : the squares of 2..i-1 have been printed

Search WWH ::

Custom Search