Java Reference

In-Depth Information

A possible loop invariant
P
can be created by making a copy of postcondition
R

and replacing the last integer
2
in it by a fresh variable:

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

How does it start?
Initially, nothing has been printed. If
k
is set to
10
, then the

invariant implies that

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

i.e. no numbers have been printed. Therefore, setting
k
to
10
truthifies
P
.

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

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

How does it make progress?
By decreasing
k
.

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

-1
.

Putting it all together, we get this loop:

//
Print
9
,
8
,
…
, down to
2

// {
invariant
P: 9
,
8
,
…
, down to
k
have been printed
}

for
(
int
k= 10; k != 2; k= k - 1)

{ System.out.println(k - 1); }

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

A different invariant, a different loop.

The loop just developed may feel a bit odd: why not start
k
at
9
, print
k
, and

stop when
k
is
1
? That would work, but it would require a different invariant. A

different invariant
P
can be created by making a copy of postcondition
R
and

replacing the last integer
2
in it by
k+1
(instead of
k
); a self-review exercise in

Sec. 7.5.5 asks you to develop a loop using this invariant.

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

7.5.4

A for-loop schema

Earlier, we presented this schema for processing the first
n
natural numbers:

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

int
k= 0;

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

while
(k != n) {

Process
k;

k= k + 1;

Lesson

page 7-4

}

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

Search WWH ::

Custom Search