Semantics of repetitions

Abstract

The reason for the inclusion of the previous chapter is that we shall use extreme solutions of equations in predicates to define the semantics of our next compound statement, known as the “repetition”. We shall first study it in its simple form, in which it is composed of a guard B and a statement S . It is denoted by surrounding the guarded statement B → S by the special bracket pair do…od . For the sake of brevity we shall call the resulting compound statement in this chapter “D0” , i.e.,

DO = do B→S od

We shall define the semantics of DO in the usual way by defining (in terms of B and S) the predicate transformers wlp.DO and wp.DO . But we shall define them differently. Were we to follow the same pattern as in the case of the straight-line programs, we would define (i) in some way the predicate transformer wlp.DO , (ii) in some way the predicate we would denote by wp.DO.true , and (iii) in terms of the previous two the predicate transformer wp.DO by

(0) [wp.DO.X = wp.DO.true Λ wlp.DO.X] for all X

Because it is more convenient, in the case of the repetition we shall follow a slightly different route: we shall define wlp.DO and wp.DO independently and then prove (0) as a consequence of those definitions. Furthermore we shall show that wlp.DO meets requirement R0 (universal conjunctivity) if wlp.S does and that wp.DO meets requirement R1 (excluded miracle) if wp.S does.