Correctness of programs - Multimedia Introduction to Programming Using Java - page 503

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.