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;
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.
Known variables
Assign to
(a) x*y = 5*4
x is 5
(b) x*y = a*b
x is a
(c) x = sum of 1..h
x is 1
(d) x = sum of 1..h
h is 2
(e) x = sum of 1..h
h is 1
x = sum of 1..h
h is 0
(g) x = sum of h..10
h is 10
(h) x = sum of h..10
h is 9
x = sum of h..10
x is 10
z is 0
x , y
z+x*y = a*b
(k) z*x y = a b
z is 1
x , y
sum of h..n = sum h..k
Search WWH ::

Custom Search