Java Reference

In-Depth Information

centrate full attention on the given preconditions, postconditions, invariants, and

other definitions. We will be brief in our explanation, for what we do here is sim-

ilar to what we did in the previous section.

As before, we find the loop invariant by replacing
n
in the postcondition by

a fresh variable
k
:

invariant:
x
is the sum of
1..k

1. How does it start?
Since
n≥1
, start with
x
equal to
1
and
k
equal to
1
.

2. When does it stop?
The invariant says that
x
is the sum of
1..k
. It stops

when
x
is the sum of
1..n
. So, it stops when
k=n
and continues as long

as
k!=n
.

3. How does it make progress?
By increasing
k
by
1
.

4. How does it fix the invariant?
By adding the next value, which is
k+1
,

to
x
.

Therefore, the loop (with initialization) is:

x= 1;

k= 1;

// {
invariant:
x
is the sum of
1..k }

while
(k != n) {

x= x + (k + 1);

k= k + 1;

}

7.2.4

Self-review exercises

SR1. How does it start?
Each case below consists of a relation and (perhaps)

values for some of the variable used in the relation. Write assignments to the

other variables that make the relation true.

Relation

Known variables

Assign to

(a)
x*y = 5*4

x
is
5

y

(b)
x*y = a*b

x
is
a

y

(c)
x =
sum of
1..h

x
is
1

h

(d)
x =
sum of
1..h

h
is
2

x

(e)
x =
sum of
1..h

h
is
1

x

(f)

x =
sum of
1..h

h
is
0

x

(g)
x =
sum of
h..10

h
is
10

x

(h)
x =
sum of
h..10

h
is
9

x

(i)

x =
sum of
h..10

x
is
10

h

(j)

z
is
0

x
,
y

z+x*y = a*b

(k)
z*x
y
= a
b

z
is
1

x
,
y

(l)

sum of
h..n =
sum
h..k

k

Search WWH ::

Custom Search