The construction of reusable components is based on the theory of structured algebraic specifications. In [Wirs 88] a notion of reusable component is developed that represents specifications at different levels of abstraction by a tree of specifications where two consecutive nodes are related by the implementation relation. Due to the fact that the nodes are ASL specifications these components can be normalized and enjoy vertical and horizontal composition properties. We are currently studying how these results can be extended to software components consisting of graphs of specifications and how functional and non-functional properties can be expressed in a type-theoretic framework.
Signature matching and the classificaton of specifications by the implementation relation help in retrieving components from a library. After matching a given abstract problem specification SP with a specification in the library, an implementation of SP can be automatically constructed from the implementation found in the library. If the matching is correct then due to the composition properties the new implementation is correct without requiring any further proof.
In [Henn 91] a formal method has been developed for integrating several module implementations to a consistent configuration of the whole system.