Java Reference

In-Depth Information

invariant:
x =
sum of
1..k-1

When
k
is
1
, this assertion looks like the precondition, when
2
, it looks like the

second assertion. And so on. This generalizing statement is the loop invariant.

We now ask our four loopy questions to help us develop the algorithm.

1. How does it start?
How do we initialize
x
and
k
so that the invariant is

true? The sequence of statements given at the beginning of the section

starts with
x = 0
. So, the sum of
1..k-1
has to be
0
, and this happens

only with
k=1
. So, the initialization is this:

x= 0;

k= 1;

2. When does it stop?
The loop can stop only when
x =
sum of
1..n-1
.

From the invariant, we know that
x =
sum of
1..k-1
. So, the loop can

stop when
k=n
. Therefore, it should continue as long as
k!=n
.

3. How does it make progress?
Variable
k
starts out at
1
and has to get up

to
n
. Therefore, progress can be made by adding
1
to
k
.

4. How does it fix the invariant?
When the repetend starts,
x
is the sum of

1..k-1
. The repetend is going to increase
k
. Before this is done, the next

value,
k
, has to be added to
x
. Thus, the invariant is fixed by executing

x= x + k;

This ends development of the loop, which is written as:

//
Store
1 + 2+ … + (n-1)
in
x

x= 0;

k= 1;

// {
invariant:
x =
sum of
1..k-1 }

while
(k != n) {

x= x + k;

k= k + 1;

}

7.2.3

A slightly different problem

In the previous section, we developed a loop that terminated with this postcon-

dition:

Activity

7-1.7

x
is the sum of
1..n-1

Here, we outline the development of a loop for a slightly different postcondition:

x
is the sum of
1..n
(where
n
≥
1
)

The purpose of writing a loop for this slightly different problem is to show

you how careful you have to be with the meanings of variables. You have to con-

Search WWH ::

Custom Search