Java Reference

In-Depth Information

This loop has a loop counter, so we can also present it as the following for-

loop schema. This schema is used often for developing loops.

//
Process natural numbers
0..n-1
, for
n≥0

// {
invariant:
0..k-1
have been processed
}

for
(
int
k= 0; k != n; k= k + 1) {

Process
k;

}

// {0..n-1
have been processed
}

7.5.5

Self-review exercises

SR1
. Write another solution to the problem in Sec. 7.5.3, but this time use this

postcondition and invariant when you answer the four loopy questions:

R: 9
,
8
,
…
, down to
2
have been printed

invariant
P: 9
,
8
,
…
, down to
k+1
have been printed

Answers to self review exercises

SR1. How does it start?
Initially, nothing has been printed. If we set
k
to
9
, then

the invariant has the meaning:

9
,
8
,
…
, down to
10
have been printed

which means that no numbers have been printed.

When does it stop?
Looking at the invariant and the postcondition, we see that

the loop should stop when
k
is
1
, so it should continue as long as
k!=1
.

How does it make progress?
By decreasing
k
.

How does it fix the invariant?
By printing the next integer, which is integer
k
.

7.6

Making progress and stopping

7.6.1

Why use condition i != n?

Suppose we have a loop like this one:

Activity

7-5.2

int i= 0;

// {
invariant:
… }

while
(i != n) {

Process
i;

i= i + 1;

}

Search WWH ::

Custom Search