Algebraic specification of modules and their basic interconnections

摘要

An algebraic specification concept for modules in software engineering is introduced which includes, in addition to a parameter and body part, explicit import and export interfaces. This concept integrates the main ideas of parameterized specifications for abstract data types and the information-hiding concept required for modules in software engineering. The concept is carefully motivated and defined with formal syntax and semantics within the framework of algebraic specifications. The basic constructions for combining modules are composition, actualization, extension, and union of modules with shared submodules. In this paper, composition and union are studied in detail. Both constructions are shown to be compositional. This means that the semantics of a combined module can be expressed in terms of the semantics of the components. To show the practical significance, specifications for the modules of an airport-schedule system and corresponding Ada packages are presented as an example.