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