Java Reference

In-Depth Information

while-rule
: Provided
Q => R
,
{
P
and
B
}
S
{
P
}
,
P
and
!B => R
,

and the loop terminates,

we conclude:
{
Q
} while
(B) S
{
R
}

The last question to answer is: how do we show that the loop terminates?

The only way it could not terminate is if the loop condition never became false,

so we need a way to prove that it does.

A
bound function
t
for a while-loop is an integer expression in the variables

used by the loop that satisfies two properties:

1. Each iteration of the loop decreases
t
, which we formalize as:

{
P && B
}
tsave= t; S
{
t < tsave
}

2. If there is another iteration to go, then t is greater than 0:

P && B => t > 0

Bound function
t
is an upper bound on the number of iterations still to be

performed. Each iteration decreases
t
by at least
1
. Further, if it ever becomes
0

(or less than
0
), then, because of point 2 and because
P
is true before and after

each iteration,
B
is false and the loop terminates. So, we have the fact that:

termination
: The loop terminates if there exists a bound function

t
for it.

At the beginning of this subsection, we showed the annotated loop, with

invariant
P
written in several places, as well as assertion
P&&!B
. To save writ-

ing so many assertions, we abbreviate and annotate the while-loop like this:

{
Q
}

//
invariant:
P:
(here we given the invariant)

//
bound function:
t
(here we give the bound function)

while
( B )

S

{
R
}

This ends our discussion of the definitions of the basic statements in terms

of Hoare triples. In the next section, we investigate developing programs using

these definitions.

IV.4

Developing simple programs

One of the important principles is that a program and its proof should be devel-

oped hand-in-hand, with the proof ideas leading the way. Further if used proper-

ly, one can even
calculate
parts of programs, instead of trying to guess them in

an
ad hoc
fashion.

Search WWH ::

Custom Search