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