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