On nondeterminacy being bounded..
This is again a very formal chapter. In the chapter "The
characterization of semantics." we have mentioned four properties that
wp(S, R)
, for any S
considered as a function of
R
, should have if its interpretation as the
weakest precondition for establishing R
is to be feasible.
(For nondeterministic mechanisms the fourth one of these was a direct
consequence of the second one.)
In the next chapter "The semantic characterization of a programming language." we have given ways for constructing new predicate transformers, pointing out that these constructions should only lead to predicate transformers enjoying the aforementioned properties (i.e. if the whole exercise is to continue to make sense). For every basic statement ("skip", "abort" and the assignment statements) one has to verify that they enjoy the said properties; for every way of building up new statements from component statements (semicolon, alternative and repetitive constructs) one has to show that the resulting composite statements enjoy those properties as well, in which demonstration one may assume that the component statements enjoy them. We verified this up to and including the Law of the Excluded Miracle for the semicolon, leaving the rest of the verifications as an exercise to the reader. We leave it at that: in this chapter we shall prove a deeper property of our mechanisms, this time verifying it explicitly for the alternative and repetitive constructs as well. (And the structure of the latter verifications can be taken as an example,for the omitted ones.)
S
and any infinite sequence of predicates
C_{0}
, C_{1}
, C_{2}
,
... such thatfor r ≥ 0 : C_{r} ⇒ C_{r+1} for all states 
(1)


(2)

For the statements "skip" and "abort" and for the assignment statements, the truth of (2) is a direct consequence of their definitions, assumption (1) not even being necessary. For the semicolon we derive
(by definition of the semantics of the semicolon)wp("S1; S2", (E r: r ≥ 0: C_{r})) =
(because Property 5 is assumed to hold for S2 )wp(S1, wp(S2, (E r: r ≥ 0: C_{r}))) =
(becausewp(S1, (E r': r' ≥ 0: wp(S2, C_{r'}))) =
S2
is assumed to enjoy Property 2, so that
wp(S2, C_{r'}) ⇒ wp(S2, C_{r'+1})
and S1
is assumed to enjoy Property 5)
(by definition of the semantics of the semicolon)(E s: s ≥ 0: wp(S1, wp(S2, C_{s}))) =

QED.

For the alternative construct we prove (2) in two steps. The easy
step is that the righthand side of (2) implies its lefthand side. For,
consider an arbitrary point X
in state space,
such that the righthand side of (2) holds,
i.e. there exists a nonnegative value s'
, say,
such that in point X
the relation wp(S, C_{s'})
holds. But because
C_{s'} ⇒ (E r: r ≥ 0: C_{r})
and any
S
enjoys Property 2 , we conclude that
holds in pointwp(S, (E r: r ≥ 0: C_{r}))
X
as well. As X
was an arbitrary state satisfying the righthand side of (2),
the latter implies the lefthand side of (2). For this argument, antecedent (1)
has not been used, but we need it for proving the implication in the other direction.
(by definition of the semantics of the alternative construct)wp(IF, (E r: r ≥ 0: C_{r})) =
(because the individualBB and (A j: 1 ≤ j ≤ n: B_{j} ⇒ wp(SL_{j}, (E r: r ≥ 0: C_{r}))) =
SL_{j}
are assumed to enjoy Property 5)

(3) 
Consider an arbitrary state X
for which (3) is true,
and let j'
be a value for j
such that B_{j'}(X) = true
; then we have in point X

(4) 
SL_{j'}
enjoys Property 2,
we conclude that


X
we also have

(5) 
s'= s'(j')
be the minimum value satisfying (5) .
We now define smax
as the maximum value of
s'(j')
taken over the (at most n
,
and therefore the maximum exists!) values
j'
for which B_{j'}(X) = true
.
In point X
then holds on account of (3) and (5)
(by definition of the semantics of the alternative construct)BB and (A j: 1 ≤ j ≤ n: B_{j} ⇒ wp(SL_{j}, C_{smax})) =
But the truth of the latter relation in statewp(IF, C_{smax}) .
X
implies there also
but as(E s: s ≥ 0: wp(IF, C_{s})) ;
X
was an arbitrary state satisfying (3) , for S = IF
the fact
that the lefthand side of (2) implies its righthand side as well, has
been proved, and thus the alternative construct enjoys Property 5 as well.
Note the essential role played by the antecadent (1) and the fact that a
guarded command set is a finite set of guarded commands.
Property 5 is proved for the repetitive construct by mathematical
induction.
Base: Property 5 holds for H_{0}
.

QED. 
H_{k}
and
H_{0}
follows that it holds for H_{k+1}
.
(by virtue of the definition ofH_{k+1}(E r: r ≥ 0: C_{r}) =
H_{k+1}
)
(because Property 5 is assumed to hold forwp(IF, H_{k}(E r: r ≥ 0: C_{r})) or H_{0}(E r: r ≥ 0: C_{r}) =
H_{k}
and for H_{0}
)
(because Property 5 holds for the alternative construct and Property 2 is enjoyed bywp(IF, (E r': r' ≥ 0: H_{k}(C_{r'}))) or (E s: s ≥ 0: H_{0}(C_{s})) =
H_{k}
)
(by virtue of the definition of(E s: s ≥ 0: wp(IF, H_{k}(C_{s}))) or (E s: s ≥ 0: H_{0}(C_{s})) =
(E s: s ≥ 0: wp(IF, H_{k}(C_{s})) or H_{0}(C_{s})) =
H_{k+1}
)

QED. 
From base and induction step we conclude that Property 5 holds for all H_{k}
, and hence
(by definition of the semantics of the repetitive construct)wp(DO, (E r: r ≥ 0: C_{r})) =
(because Property 5 holds for all(E k: k ≥ 0: H_{k}(E r: r ≥ 0: C_{r})) =
H_{k}
)
(because this expresses the existence of a(E k: k ≥ 0: (E s: s ≥ 0: H_{k}(C_{s}))) =
(k, s)
pair)
(by definition of the semantics of the repetitive construct)(E s: s ≥ 0: (E k: k ≥ 0: H_{k}(C_{s}))) =

QED. 
Property 5 is of importance on account of the semantics of the repetitive construct
such a precondition could be the postcondition for another statement. Becausewp(DO, R) = (E k: k ≥ 0: H_{k}(R))) ;
for k ≥ 0 : 
H_{k}(R) ⇒ H_{k+1}(R) 
for all states , 
BB
holds
is equivalent todo B_{1} → SL_{1} ⌷ B_{2} → SL_{2} ⌷ ... ⌷ B_{n} → SL_{n} od
(In initial states in which BB, does not hold, the first program would have acted as "skip", the secend one as "abort".) That is, we have to prove thatif B_{1} → SL_{1} ⌷ B_{2} → SL_{2} ⌷ ... ⌷ B_{n} → SL_{n} fi;
do B_{1} → SL_{1} ⌷ B_{2} → SL_{2} ⌷ ... ⌷ B_{n} → SL_{n} od .
(BB and wp(DO, R)) = (BB and wp(IF, wp(DO, R))) .
(on account of the semantics of the repetitive construct)BB and wp(IF, wp(DO, R)) =
(because Property 5 holds forBB and wp(IF, (E k: k ≥ 0: H_{k}(R))) =
IF
)
(becauseBB and (E s: s ≥ 0: wp(IF, H_{s}(R))) =
(BB and H_{0}(R)) = F
)
(on account of the recurrence relation for theBB and (E s: s ≥ 0: wp(IF, H_{s}(R)) or H_{0}(R)) =
H_{k}(R)
)
(becauseBB and (E s: s ≥ 0: H_{s+1}(R)) =
(BB and H_{0}(R)) = F
)
(on account of the semantics of the repetitive construct)BB and (E k: k ≥ 0: H_{k}(R)) =
BB and wp(DO, R) . QED.
Finally, we would like to draw attention to a very different consequence of the fact that all our mechanisms enjoy Property 5 . We could try to make the program S: "set x
to any positive integer" with the properties:
a) 
wp(S, X > 0) = T 
b) 
(A s: s ≥ 0: wp(S, 0 ≤ x < s) = F) . 
S
is guaranteed
to terminate with x
equal to some positive value, property b) expresses that
S
is a mechanism of unbounded nondeterminacy, i.e. that no a priori upper
bound for the final value of x
can be given. For such a program S
,
we could, however, derive now:
T = wp(S, X > 0)
= wp(S, (E r: r ≥ 0: 0 ≤ x < r))
= (E s: s ≥ 0: wp(S, 0 ≤ x < s))
= (E s: s ≥ 0: F)
= F .
This, however, is a contradiction: for the mechanism
S: "set x
to any positive integer"
no program exists!
As a result, any effort to write a program for
"set x
to any positive integer" must fail.
For insiance, we could consider:
This construct will continue to increasego on:= true; x:= 1;
do go on → x:= x + 1
▯ go on → go on:= false
od .
x
as long as the first alternative
is chosen; as soon as the second alternative has been chosen once, it terminates
immediately. Upon termination x
may indeed be "any positive integer" in the
sense that we cannot think of a positive value X
such that termination with
x = X
is impossible. But termination is not guaranteed either!
We can enforce termination: with N
some large, positive constant we can write
but then property b) is no longer satisfied.go on:= true; x:= 1;
do go on and x < N → x:= x + 1
▯ go on → go on:= false
od
The nonexistence of a program for "set x
to any positive integer"
is reassuring in more than one sense. For, if such a program could exist, our
definition of the semantics of the repetitive construct would have been subject
to doubt, to say the least. With
our formalism for the repetitive construct givesS: do x > 0 → x:= x − 1
▯ x < 0 → "set x to any positive integer"
od
wp(S, T) = (x ≥ 0)
, while
I expect most of my readers to conclude that under the assumption of the
existsnce of "set x
to any positive integer" for
x < 0
termination would be guaranteed as well.
But then the interpretation of wp(S, T)
as the weakest
precondition guaranteeing termination would no longer be justified. But when
we substitute our first wouldbe implementation:
S: do x > 0 → x:= x − 1
▯ x < 0 → go on:= true; x:= 1;
do go on → x:= x + 1
▯ go on → go on:= false
od
od
wp(S, T)= (x ≥ 0)
is fully correct, both intuitively and formally.
The second reason for reassurance is of a rather different nature: a mechanism of unbounded nondeterminacy but yet guaranteed to terminate would be able to make within a finite time a choice out of infinitely many possibilities: if such a mechanism could be formulated in our programming language, that very fact would present an unsurmountable barrier to the possibility of the implementatlon of that programming language.
Acknowledgement. I would like to express my great indebtness to John C.Reynolds
for drawing my attention to the central role of Property 5 and to the fact that
the nonexistence of a mechanism "set x
to any positive
integer" is essential
for the intuitive justification of the semantics of the repetitive construct.
He is, of course, in no way to be held responsible for any of the above. (End
of acknowledgement.)