Java Reference
In-Depth Information
// { condition and invariant are true }
// { invariant is true }
Developing a second loop
We develop a second loop, which stores the sum of the first n-1 positive num-
bers in int variable x , for some n≥1 . Here is a subtle point: if n is 1 , then we
want to store the sum of the first 0 numbers in x . That is why we assign 0 to x as
a separate step:
// Store 1+2+…+(n-1) in x (assuming n≥1 )
x= 0;
x= x + 1;
x= x + 2;
x= x + (n - 1);
We develop a loop that is equivalent to this sequence of assignments.
Developing the loop invariant
The first task is to annotate this sequence so that we can derive a suitable
loop invariant. We start by writing a postcondition. The postcondition is easily
derived from the task of the segment, to store 1+2+…+(n-1) in x :
// { x = sum of 1..n-1 }
Working backward from the postcondition, we fill in the other assertions:
// { precondition: x = sum of 1..1-1 }
x= x + 1;
// { x = sum of 1..2-1 }
x= x + 2;
// { x = sum of 1..3-1 }
// { x = sum of 1..(n-1)-1) }
x = x + (n-1);
// { postcondition: x = sum of 1..n-1 }
Note that they all have the same form: the upper end of the range is an
expression of the form v-1 for some value v . Making them all have the same
form is important for finding an invariant.
Like the previous example, the precondition may seem a bit odd. Again, this
useful convention allows us to write assertions in a consistent manner.
A relation that generalizes all these assertions can be found by generalizing
the postcondition: make a copy of the postcondition and replace identifier n by a
fresh (that is, new) variable, say k :
Search WWH ::

Custom Search