Reasoning about software systems developed using components begins with component-level specifications,
from which system-level specifications are derived. While sound compositional reasoning is a strength of
formal specification methods, practical experience with systems construction leads us to expect surprises
when two components that were never intended to be combined are composed. Component specifications,
like any other human artifact, are likely to be in error. Composition throws the mistakes in one component
against those in another, leading to unexpected and often bizarre behavior.
We review the theory of formal software specification and apply it to the combination of component specifica-
tions into system-level properties, where deficiencies in component specifications can be strangely reflected.
We conclude that desirable properties of system specifications do not always arise from those same properties
at the component level.
Keywords: Formal specification, software component, composition
Although elementary formal descriptions of program semantics, specifications, and
the correctness relationship between them have long been used, applying these de-
scriptions to software components and their combination into systems has been
little explored. Furthermore, the role played by persistent state in software has not
been singled out for formal analysis. State plays a central role in component-based
system development (CBSD), so CBSD is a good setting for a theoretical treatment.