×

Algebraic specification of modules and their basic interconnections. (English) Zbl 0619.68027

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.

MSC:

68P05 Data structures
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] “‘The Programming Language Ada,” Reference Manual, (Lect. Notes in Comput. Sci., Vol. 106 (1981), Springer-Verlag: Springer-Verlag New York/Berlin)
[2] Goguen, J. A.; Thatcher, J. W.; Wagner, E. G., An initial algebra approach to the specification, correctness and implementation of abstract data types, (Yeh, R. T., Current Trends in Prog. Method., IV: Data Structuring (1978), Prentice-Hall: Prentice-Hall Englewood Cliffs, N.J), 80-149
[3] Ehrig, H.; Kreowski, H.-J.; Thatcher, J. W.; Wagner, E. G.; Wright, J. B., Parameter passing in algebraic specification languages, (Proceedings, Aarhus Workshop on Program Specification. Proceedings, Aarhus Workshop on Program Specification, 1981. Proceedings, Aarhus Workshop on Program Specification. Proceedings, Aarhus Workshop on Program Specification, 1981, Lect. Notes in Comput. Sci., Vol. 134 (1982), Springer-Verlag: Springer-Verlag New York/Berlin), 322-369
[4] Blum, E. K., An Abstract System Model of Ada Semantics, TRW Technical Report (Aug. 1984)
[5] Blum, E. K.; Parisi-Presicce, F., Implementation of data types by algebraic methods, J. Comput. System Sci., 27, No. 2, 304-330 (1983) · Zbl 0537.68026
[6] Blum, E. K.; Parisi-Presicce, F., The semantics of shared submodule specifications, (Proceedings, CAAP 85. Proceedings, CAAP 85, Lect. Notes in Comput. Sci., Vol. 185 (1985), Springer-Verlag: Springer-Verlag New York/Berlin), 359-373 · Zbl 0563.68014
[7] Bothe, K., A Generalized Abstract Data Type Concept (1980), Sektion Mathematik, Humboldt Universitat: Sektion Mathematik, Humboldt Universitat Berlin, Preprint No. 3 · Zbl 0469.68025
[8] Ehrig, H., Parameterized specifications with requirements, (Proceedings, CAAP ’81. Proceedings, CAAP ’81, Lect. Notes in Comput. Sci., Vol. 112 (1981), Springer-Verlag: Springer-Verlag New York/Berlin), 1-24
[9] Ehrig, H.; Fey, W.; Hansen, H., ACT ONE: An Algebraic Specification Language with Two Levels of Semantics, (Technical Report No. 83-03 (1983), Tech. Univ: Tech. Univ Berlin) · Zbl 0549.68010
[10] Ehrig, H.; Fey, W.; Parisi-Presicce, F.; Blum, E. K., Algebraic theory of module specifications with constraints, (Proceedings, Math. Found. of Comput. Sci.. Proceedings, Math. Found. of Comput. Sci., Lect. Notes in Comput. Sci., Vol. 233 (1986), Springer-Verlag: Springer-Verlag New York/Berlin), 59-77 · Zbl 0602.68021
[11] Ehrig, H.; Fey, W.; Parisi-Presicce, F., Distributive laws for composition and union of module specifications for software systems, (Proceedings IFIP TC2 Work. Conf. on Program Specification and Transformation. Proceedings IFIP TC2 Work. Conf. on Program Specification and Transformation, Bad Tölz (April 1986)) · Zbl 0602.68021
[12] Ehrig, H.; Kreowski, H.-J., Compatibility of parameter passing and implementation of parameterized data types, Theoret. Comput. Sci., 27, 255-286 (1983) · Zbl 0553.68015
[13] Ehrig, H.; Kreowski, H.-J.; Mahr, B.; Padawitz, P., Algebraic implementations of abstract data types, Theoret. Comput. Sci., 20, No. 3, 209-264 (1982) · Zbl 0483.68018
[14] Ehrig, H.; Mahr, B., Fundamentals of Algebraic Specifications 1: Equations and Initial Semantics, (EACTS Monographs on Theoret. Comput. Sci., Vol. 6 (1985), Springer-Verlag: Springer-Verlag New York/Berlin) · Zbl 0557.68013
[15] Ehrig, H.; Weber, H., Algebraic specification of modules, (Neuhold, E. J.; Chronist, G., Formal Models in Programming (1985), North-Holland: North-Holland Amsterdam), 231-258
[16] Guttag, J. V.; Horning, J. J.; Wing, J. M., Larch in Five Easy Pieces, (Technical Report No. 5 (July 1985), Digital Systems Research Center) · Zbl 0581.68008
[17] Goguen, J. A.; Burstall, R. M., Introducing institutions, (Proc. Logics of Programs. Proc. Logics of Programs, Lect. Notes in Comput. Sci., Vol. 164 (1984), Springer-Verlag: Springer-Verlag New York/Berlin), 221-256 · Zbl 1288.03001
[18] Goguen, J. A.; Meseguer, J., Universal realization, persistent interconnection and implementation of abstract modules, (Proceedings, 9th ICALP. Proceedings, 9th ICALP, Lect. Notes in Comput. Sci., Vol. 140 (1982), Springer-Verlag: Springer-Verlag New York/Berlin), 265-281 · Zbl 0493.68014
[19] Giarratana, V.; Gimona, F.; Montanari, U., Observability concepts in abstract data type specifications, (5th Symp. Math. Found. of Comp. Sci.. 5th Symp. Math. Found. of Comp. Sci., 1976. 5th Symp. Math. Found. of Comp. Sci.. 5th Symp. Math. Found. of Comp. Sci., 1976, Lect. Notes in Comput. Sci., Vol. 45 (1976), Springer-Verlag: Springer-Verlag New York/Berlin), 576-587 · Zbl 0338.68023
[20] Kapur, D., Toward a Theory of Abstract Data Types, (Report TR-237 (1980), Lab. for Comput. Sci., MIT)
[21] Lipeck, U., Ein algebraischer Kalkul fur einen Strukturierten Entwurf von Datenabstractionen, (Ph.D. Thesis (1982), Univ. Dortmund) · Zbl 0506.68023
[22] Liskov, B. H.; Zilles, S. N., Specification techniques for data abstracton, IEEE Trans. Software Engrg., SE-1, No. 1, 7-19 (1975)
[23] Majster, M. E., Limits of the algebraic specification of data types, SIGPLAN Notices, 12, No. 10, 37-42 (1977) · Zbl 0348.68026
[24] F. Parisi-Presicce “Union and Actualization of Module Specifications: Some Compatibility Results,” J. Comput. System Sci., to appear.; F. Parisi-Presicce “Union and Actualization of Module Specifications: Some Compatibility Results,” J. Comput. System Sci., to appear. · Zbl 0623.68017
[25] Parisi-Presicce, F., Inner and mutual compatibility of basic operations on module specifications, (Proceedings CAAP 86. Proceedings CAAP 86, Lect. Notes in Comput. Sci., Vol. 214 (1986), Springer-Verlag: Springer-Verlag New York/Berlin), 30-44 · Zbl 0589.68017
[26] Parnas, D. L., A technique for software module specification with examples, Comm. ACM, 15, No. 5, 330-336 (1972)
[27] Reichel, H., Behavioral equivalence—A unifying concept for initial and final specification methods, (Proceedings, 3rd Hungarian Comput. Sci. Conf.. Proceedings, 3rd Hungarian Comput. Sci. Conf., Budapest (1981)), 27-39
[28] Schoett, O., A Theory of program modules, their specification and implementation, (draft report (1982), Univ. Edinburgh)
[29] Sannella, D.; Wirsing, M., A Kernel Language for Algebraic Specification and Implementation, (Internal Report No. CSR-131-83 (1983), Univ. Edinburgh), 1-44
[30] Weber, H.; Ehrig, H., Specification of modular systems, Trans. Software Engrg (June 1986)
[31] Wirth, N., Programming in Module-2 (1982), Springer-Verlag: Springer-Verlag New York
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.