TABLE OF CONTENTS At the top level of a main imperative program, any system can be built up inductively using the three elementary structured-programming constructions of sequence, conditional, and iteration. The standard software analysis paradigm is to:
Obtain a general rule for analysis of each elementary construction in isolation, then
Perform the system analysis piece by piece, using the algebra of recursive construction for a given system.
In this way, the largest system is no more difficult to analyze than the simplest it just takes more applications of the three elementary-construction rules.
Section 6.5 gives the theory for sequences, which turns out to be the essence of the theory. The system-design constructions of conditional and iteration can be analyzed by turning them into special cases of sequences.
The sequential construction of Section 6.5 can be applied to a conditional that appears following a component B:
The conditional test b partitions the input domain D into:
First consider B; C T, which can be analyzed using equation (6.1) with subdomains 
, but in calculating the set in the numerator of equation (6.1), count a point z only if b(B(z)) is true. This is equivalent to intersecting the subdomains of C T with D T. Similarly, treat B; C F with C F s subdomains adjusted to include only the part of each where b is false. These two calculations determine the contribution from C T
