On Formal Specification of Software Components and Systems

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 specifications 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.