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