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 pre-condition for establishing R is to be feasible. (For non-deterministic 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 C0 , C1 , C2 , ... such thatfor r ≥ 0: Cr ⇒ Cr+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: Cr)) =
(because Property 5 is assumed to hold for S2 )wp(S1, wp(S2, (E r: r ≥ 0: Cr))) =
(becausewp(S1, (E r': r' ≥ 0: wp(S2, Cr'))) =
S2 is assumed to enjoy Property 2, so that wp(S2, Cr') ⇒ wp(S2, Cr'+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, Cs))) =
|
QED.
|
For the alternative construct we prove (2) in two steps. The easy step is that the right-hand side of (2) implies its left-hand side. For, consider an arbitrary point X in state space, such that the right-hand side of (2) holds, i.e. there exists a non-negative value s', say, such that in point X the relation wp(S, Cs') holds. But because Cs' ⇒ (E r: r ≥ 0: Cr) and any S enjoys Property 2 , we conclude that
holds in pointwp(S, (E r: r ≥ 0: Cr))
X as well. As X was an arbitrary state satisfying the right-hand side of (2), the latter implies the left-hand 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: Cr)) =
(because the individualBB and (A j: 1 ≤ j ≤ n: Bj ⇒ wp(SLj, (E r: r ≥ 0: Cr))) =
SLj 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 Bj'(X) = true ; then we have in point X
|
(4) |
SLj' 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 Bj'(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: Bj ⇒ wp(SLj, Csmax)) =
But the truth of the latter relation in statewp(IF, Csmax) .
X implies there also
but as(E s: s ≥ 0: wp(IF, Cs)) ;
X was an arbitrary state satisfying (3) , for S = IF the fact that the left-hand side of (2) implies its right-hand 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 H0.
|
QED. |
Hk and H0 follows that it holds for Hk+1 .
(by virtue of the definition ofHk+1(E r: r ≥ 0: Cr) =
Hk+1)
(because Property 5 is assumed to hold forwp(IF, Hk(E r: r ≥ 0: Cr)) or H0(E r: r ≥ 0: Cr) =
Hk and for H0)
(because Property 5 holds for the alternative construct and Property 2 is enjoyed bywp(IF, (E r': r' ≥ 0: Hk(Cr'))) or (E s: s ≥ 0: H0(Cs)) =
Hk)
(by virtue of the definition of(E s: s ≥ 0: wp(IF, Hk(Cs))) or (E s: s ≥ 0: H0(Cs)) =
(E s: s ≥ 0: wp(IF, Hk(Cs)) or H0(Cs)) =
Hk+1)
|
QED. |
From base and induction step we conclude that Property 5 holds for all Hk , and hence
(by definition of the semantics of the repetitive construct)wp(DO, (E r: r ≥ 0: Cr)) =
(because Property 5 holds for all(E k: k ≥ 0: Hk(E r: r ≥ 0: Cr)) =
Hk )
(because this expresses the existence of a(E k: k ≥ 0: (E s: s ≥ 0: Hk(Cs))) =
(k, s)-pair)
(by definition of the semantics of the repetitive construct)(E s: s ≥ 0: (E k: k ≥ 0: Hk(Cs))) =
|
QED. |
Property 5 is of importance on account of the semantics of the repetitive construct
such a pre-condition could be the post-condition for another statement. Becausewp(DO, R) = (E k: k ≥ 0: Hk(R))) ;
for k ≥ 0: |
Hk(R) ⇒ Hk+1(R) |
for all states , |
BB holds
is equivalent todo B1 → SL1 ⌷ B2 → SL2 ⌷ ... ⌷ Bn → SLn 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 B1 → SL1 ⌷ B2 → SL2 ⌷ ... ⌷ Bn → SLn fi;
do B1 → SL1 ⌷ B2 → SL2 ⌷ ... ⌷ Bn → SLn 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: Hk(R))) =
IF)
(becauseBB and (E s: s ≥ 0: wp(IF, Hs(R))) =
(BB and H0(R)) = F )
(on account of the recurrence relation for theBB and (E s: s ≥ 0: wp(IF, Hs(R)) or H0(R)) =
Hk(R) )
(becauseBB and (E s: s ≥ 0: Hs+1(R)) =
(BB and H0(R)) = F )
(on account of the semantics of the repetitive construct)BB and (E k: k ≥ 0: Hk(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 non-determinacy, 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 non-existence 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 pre-condition guaranteeing termination would no longer be justified. But when we substitute our first would-be 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 non-determinacy 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 non-existence 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.)