EWD249 - 22

the effect is regarded as being established by a primitive action.

When we do take a number of intermediate states into consideration this means that we have parsed the happening in time. We regard it as a sequential computation, i.e. the time-succession of a number of subactions and we have to convince ourselves that the cumulative effect of this time-succession of subactions indeed equals the desired net effect of the total computation.

The simplest case is a parsing, a decomposition, into a fixed number of subactions that can be enumerated. In flowchart form this can be represented as follows.

                    |
                    v
      +- - - - - - - - - - -+
      |    +---------+      |
      |    |   S1    |      |
      |    +---------+      |
      |         |           |
      |    +---------+      |
      |    |   S2    |      |
      |    +---------+      |
      |         :           |
      |         :           |
      |    +---------+      |
      |    |   Sn    |      |
      |    +---------+      |
      +- - - - - - - - - - -+
                    |
                    v

        S1; S2; ......; Sn

The validity of this decomposition has to be established by enumerative reasoning. In this case, shortening of the conceptual gap between program and computation can be achieved by requiring that a linear piece of program text contains names or descriptions of the subactions in the order in which they have to take place. In our earlier example (invariance of 0 ≤ r < dd)

"dd:= dd / 2;
 if dd ≤ r do r:= r - dd"

this condition is satisfied. The primary decomposition of the computation is into a time-succession of two actions; in the program text we recognize this structure

"halve dd;
 reduce r modulo dd" .

We are considering all initial states satisfying 0 ≤ r < dd and in all computations then considered, the given parsing into two subactions is applicable.