Algebraic concepts for formal specification and transformation of modular software systems

The role of formal methods for software specification and transformation is discussed, and it is shown how algebraic concepts can support the software development process. Algebraic specification techniques in general are discussed, as are the formal specification languages Act One and Lotos for data types, software systems, and distributed systems. The specification languages are introduced together with an environment of tools developed within the ESPRIT projects Sedos and Lotosphere. Specification and transformation for modular software systems are supported by the concept of algebraic module specification, including mechanisms for horizontal structuring, which is built in Act Two, and vertical refinement. Compatibility results for horizontal and vertical development steps are given and applied to modular specification development of a parts system