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;