Theories of Programming: Top-Down and Bottom-Up and Meeting in the Middle - Correct System Design: Recent Insights and Advances - page 7

the predicate describing . Since

we can identify programs and specications with their corresponding predicates,
correctness is nothing but the familiar logical implication

P logically implies the predicate describing S

P ) S

For example, the specication of non-decreasing x is met by a program that

increments x , as may be checked by a proof of the implication

ok ^

!
ok

!
x^ x < max ^ x := x +1 ) x

This simple notion of correctness is obviously correct, and is completely general
to all top-down theories of programming. Furthermore it validates in complete
generality all the normal practices of software engineering methodology. For
example, stepwise design develops a program in two (or more) steps. On a par-
ticular step, the engineer produces a design D which describes the properties of

the eventual program , but

leaving further details of the eventual program to be decided in later steps. The
general design method is dened and justied by the familiar cut rule of logic,
expressing the mathematical property of transitivity of logical implication

P in somewhat greater detail than the specication S

D ) S P)D
P)S

In words this rule may be read: if the design is correct relative to the specication,
and if the program meets its design requirement, then the program also meets
its original specication.
The most useful method of constructing the specication of a large system
is as the conjunciton of its many requirements. Programs and designs can also
be combined by conjunction, provided that they have completely disjoint alpha-
bets. In that case, the conjunction can generally be implemented by parallel
execution of its operands. Such a parallel implementation is also possible when
programs share parts of their alphabet, provided that these include observa-
tions of all the ways in which the programs can interact with each other during
their execution. In these cases, the stepwise approach to implementation can
be greatly strengthened if each step is accompanied by a decomposition of the
design D 2 . The correctness of

the decomposition can be checked before implementation starts by proof of the
implication

D into separately implementable parts D 1 and

D 1 ^ D 2 ) D

Further implementation of the designs D 2 can be progressed indepen-

dently and even simultaneously to deliver components

D 1 and

P 2 . When the
components are put together they certainly will meet the original design re-
quirement

P 1 and

. The proof principle that justies the method of design by parts is
just the expression of the monotonicity of conjunction with respect to implication

D