Java Reference
In-Depth Information
// {
condition
and
invariant
are true
}
repetend
// {
invariant
is true
}
7.2.2
Developing a second loop
We develop a second loop, which stores the sum of the first
n-1
positive num-
bers in
int
variable
x
, for some
n≥1
. Here is a subtle point: if
n
is
1
, then we
want to store the sum of the first
0
numbers in
x
. That is why we assign
0
to
x
as
a separate step:
Activity
7-1.4
//
Store
1+2+…+(n-1)
in
x
(assuming
n≥1
)
x= 0;
x= x + 1;
x= x + 2;
…;
x= x + (n - 1);
We develop a loop that is equivalent to this sequence of assignments.
Developing the loop invariant
The first task is to annotate this sequence so that we can derive a suitable
loop invariant. We start by writing a postcondition. The postcondition is easily
derived from the task of the segment, to store
1+2+…+(n-1)
in
x
:
// { x =
sum of
1..n-1 }
Working backward from the postcondition, we fill in the other assertions:
// {
precondition:
x =
sum of
1..1-1 }
x= x + 1;
// { x =
sum of
1..2-1 }
x= x + 2;
// { x =
sum of
1..3-1 }
…
// { x =
sum of
1..(n-1)-1) }
x = x + (n-1);
// {
postcondition:
x =
sum of
1..n-1 }
Note that they all have the same form: the upper end of the range is an
expression of the form
v-1
for some value
v
. Making them all have the same
form is important for finding an invariant.
Like the previous example, the precondition may seem a bit odd. Again, this
useful convention allows us to write assertions in a consistent manner.
A relation that generalizes all these assertions can be found by generalizing
the postcondition: make a copy of the postcondition and replace identifier
n
by a
fresh (that is, new) variable, say
k
:
Search WWH ::
Custom Search