Java Reference
In-Depth Information
0..(k+1)-1
”
>
x = (
sum of squares of
0..(k+1)-1) - k*k
= <
Rearrange
>
x + k*k = (
sum of squares of
0..(k+1)-1)
The last formula has the desired form,
[x,k\E,k+1]P
, where
E
is
x + k*k
.
Thus, the Hoare triple can be written as follows:
{
P
}
x, k= x +
k*
k, k+1;
{
P
}
In this case, we wanted to increment
k
and had to determine what to assign
to
x
so that
P
would be maintained. We did not guess what to assign to
x
; we cal-
culated it. We moved the problem away from programming into the realm of
logic and arithmetic.
This problem is so simple that perhaps calculation is not necessary to solve
it. However, in many cases, such calculation can save the time of repeatedly
guessing and testing until one has, by chance, discovered the right expression
E
.
An example of this appears in Sec. IV.6.
IV.5
Developing loops
Chapter 7 discusses the development of a loop:
{
Q
}
//
invariant:
P
//
bound function:
t
while
( B )
S
{
R
}
in terms of four loopy questions:
1. How does it start? (The initialization should truthify
Q
.)
2. When does it end? (
P&&!B
should imply
R
.)
3. How does it make progress? (Each iteration must reduce
t
.)
4. How does it fix the invariant? (the repetend must satisfy
{
P&&B
}
S
{
P
}
.)
Each of the four loopy questions deals with one of the premises of the while-
loop inference rule. Chapter 7 dealt informally with termination rather than use
a bound function. So, Chap. 7 was really working with this inference rule. In
Chaps. 7 and 8, many loops were developed using the four loopy questions.
Therefore, in this section, we discuss only two issues: (1) how to find invari-
ants and (2) how to develop the repetend of a loop.
IV.5.1
Developing the invariant
Below is the fully annotated while-loop. This annotation shows us that invariant
Search WWH ::
Custom Search