Abstract:
Compositional design is concerned with both constructing systems by
composing components and with deconstructing systems into proposed
sets of components. In bottom-up design, engineers prove system
properties given properties of components and a compositional
structure. In top-down design, they propose properties of components
and a compositional structure given system properties. In this paper
we show how the theory of predicate transformers, which has been used
so successfully in sequential programming, can be applied to
compositional design of systems. The rules of composition we study
are more general than the rules employed in sequential programming,
and the systems we study are not limited to programs. We exploit
theorems about weakest and strongest solutions to equations to obtain
a collection of useful predicate transformers, and then we exploit the
theory of conjugate transformers to obtain more useful transformers.
We show how these transformers are useful for both bottom-up and
top-down design.
Michel Charpentier <
>
Last modified: Fri Apr 21 14:06:15 EDT 2000