Java Reference

In-Depth Information

Process
0;

Process
1;

…

Process
n-1;

We can easily write down a postcondition for the loop:

See lesson page

7-3 to obtain

the schema.

0..n-1
have been processed

To develop a loop invariant, we make a copy of the postcondition and replace
n

in it by a fresh variable
k
:

invariant:
0..k-1
have been processed

How does it start?
The invariant has the nice property that assigning
0
to
k

truthifies it, because the invariant then means that no natural numbers have been

processed.

When does it stop?
The loop should stop when
k=n
because then the

invariant implies that the postcondition is true. So, the loop should continue as

long as
k!=n
.

How does it make progress?
Variable
k
starts out at
0
and is supposed to

end up at
n
, so to make progress, increment
k
.

How does it fix the invariant?
Since
k
is being incremented, the next num-

ber must be processed. The invariant tells us that the next number is
k
.

This leads to the loop schema of Fig. 7.2.

7.4.2

A loop to count the w's

We write a loop to count the number of
w
's in a string
s
, starting with the schema

of Fig. 7.2. We can use this schema because the task is to process the characters

of
s
, and these have numbers in the range
0..s.length()-1
, so we are really

processing the integers in this range.

The first step is to rewrite the schema in the context of our problem. We

begin by replacing
n
in the schema by
s.length()
.

Activity

7-3.2

//
Process the
n
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;

}

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

Figure 7.2:

A schema to process natural numbers
0..n-1

Search WWH ::

Custom Search