Java Reference

In-Depth Information

SR2. When does it stop?
Each case below consists of an invariant and a post-

condition. It is known that the invariant is true. What extra condition is needed

to know that the postcondition is true?

invariant postcondition

(a)
x
is sum of
1..k x
is sum of
1..10

(b)
x
is sum of
1..k x
is sum of
1..n

(c)
x
is sum of
0..k-1 x
is sum of
0..10

(d)
x
is sum of
1..k-1 x
is sum of
1..n

(e)
x
is sum of
0..k-1 x
is sum of
0..n-1

(f)
x
is sum of
h..k x
is sum of
1..k

(g)
x
is sum of
h..k-1 x
is sum of
1..k-1

(h)
m
is the average of
h..k-1 x
is the average of
1..k-1

(i)
m
is the average of
1..k-1 m
is the average of
1..n-1

(j)
z+x*y = a*b x*y = a*b

(k)
z+x*y = a*b z = a*b

(l)
h..k-1
has been processed
1..k-1
has been processed

SR3. How does it make progress?
Each case below consists of an initial value

for a variable and a final value. Write down a simple assignment that gets the

variable closer to its final value.

initial value final value

(a)
h
is
0 h
is
10

(b)
h
is
10 h
is
0

(c)
h
is
n
(where
n>0
)
h
is
0

(d)
h
is
n
(where
n<0
)
h
is
0

SR4. How does it fix the invariant?
Each case below contains a relation that is

assumed to be true and a statement that changes a variable. Write down a state-

ment to execute
before
the given statement so that after both are executed, the

relation is still true.

relation

statement

(a)
s
is the sum of
1..h

h= h + 1;

(b)
s
is the sum of
1..h-1

h= h + 1;

(c)
s
is the sum of
k..n

k= k - 1;

(d)
s
is the sum of
k+1..n

k= k - 1;

(e)
s
is the sum of
1..h

h= h - 1;

(f)

z+x*y = 100

y= y-1;

(g)
z+x*y = 100
and
y
is even and
y>0

y= y/2;

Answers to self-review exercises

SR1.
(a)
y = 4
, (b)
y = b
, (c)
h = 1
, (d)
x = 3
, (e)
x = 1
, (f)
x = 0
, (g)
x =

10
, (h)
x = 19
, (i)
h = 10
,(j)
x = a
,
y = b
, (k)
x = a
,
y = b
, (l)
k = n
.

SR2.
(a)
k=10
, (b)
k=n
, (c)
k-1=10
, (d)
k-1=n
, (e)
k=n
, (f)
h=1
,. (g)
h

Search WWH ::

Custom Search