Abstract
Module, import, export and detail hiding are well-known notions in software engineering. If algebraic specifications together with their operational semantics of term rewriting should be useful as a programming language, similar concepts must be developed to cope with very large specifications. Especially the concept of detail hiding is important, since many problems and their efficient solutions require hidden sorts or hidden functions.
In this paper we discuss a module concept for algebraic specifications. A module consists of an algebraic specification, the body specification, together with import and export specifications. The semantics is given by a free functor from the class of import algebras to the class of body algebras followed by a subalgebra restriction according to the export signature. A module is correct, if its semantics does not change the reexport part of any import algebra. The reexport specification is the common part of import and export specifications. This requirement is much weaker than the requirements for module correctness we find in other approaches, e.g. in [EW
This makes module specifications more suitable for software engineering purposes. For instance there is no need for explicit error handling in the body specification if the export restricts data to non-error data only. The example of a specification of a process scheduler demonstrates the usefulness of this concept. On the other hand, theoretic results concerning correctness of the semantics can be carried over to the new module concept. In this paper, we show that some basic constructions on modules preserve correctness and that the composition of correct modules yields a correct module.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
7. References
Bidoit, M., Choppy, C., Voisin, F.: The ASSPEGIQUE Specification Environment, in: Kreowski, H.-J. (ed.): Informatik Fachberichte Nr. 116, Springer, Berlin, 1985
Blum, E.K., Ehrig, H., Parisi-Presicce, F.: Algebraic Specification of Modules and Their Basic Interconnections, JCSS 34 (1987), 293–339
Ehrig, H., Fey, W., Hansen, H., Löwe, M., Parisi-Presicce, F.: Algebraic Theory of Modular Specification Development, Research Report No. 87-06, Techn. Univ. of Berlin, 1987
Ehrig, H., Mahr, B.: Fundamentals of Algebraic Specification 1, Springer, Berlin, 1985
Ehrig, H., Mahr, B.: Fundamentals of Algebraic Specification 2, Springer, Berlin, 1988 (to appear)
Ehrig, H., Weber, H.: Programming in the Large with Algebraic Module Specifications, Proc. IFIP Congress 1986, Dublin, 1986
Futatzugi, K., Goguen, J.A., Jouannaud, J.P., Meseguer, G.: Principles of OBJ2, in: Proc. of the 12. ACM Symposium on Principles of Programming Languages, New Orleans, Lousiana (1985), 52–66
Gogolla, M.: On Parametric Algebraic Specifications with Clean Error Handling, in: Proc. of the Int. Joint Conf. on Theory and Practice of Software Development, Pisa, Italy (LNCS 249), 1987
Goguen, J.A.: Reusing and Interconnecting Software Components, Computer 19, 2 (Feb. 1986), 16–28
Goguen, J.A., Meseguer, J.: Order Sorted Algebra I: Partial and Overloaded Operations, Errors and Inheritance, (to appear) SRI International Computer Science Lab, 198
Hansen, H., Löwe, M.: A New Module Concept for Algebraic Specifications, Internal Report, Techn. University of Berlin, 1988
Harper, R., MacQueen, D., Milner, R.: Standard ML, LFCS Report Series No. ECS-LFCS-86-2, Department of Computer Science, Univ. of Edinburgh, 1986
Hussmann, H.: Rapid Prototyping for Algebraic Specifications — RAP Systems User Manual, Univ. of Passau, Research Report MIP-8504, 1985
Parisi-Presicce, F.: Partial Composition and Recursion of Module Specifications, in: Proc. of the Int. Joint Conf. on Theory and Practice of Software Development, Pisa, Italy, (LNCS 249), 1987, 217–231
Parisi-Presicce, F.: Iteration of Module Specifications, to appear in: Proc. of CAAP'88, Nancy, France, March 1988
Reichel, H.: Behavioural Program Specification, in: Proc. Category Theory and Computer Programming, Guildford, September 1985, LNCS 240, pp. 390–411
Sanella, D., Wirsing, M.: A Kernal Language for Algebraic Specification and Implementation, Internal Report No. CSR-131-83, Univ. of Edinburgh, 1–44; (extended abstract) also in: Proc. Int. Conf. on Foundations of Computing Theory, Borgholm, Sweden, Springer LNCS 158, 413–427
Wirth, N.: Programming in Modula 2, Springer, Berlin, 1985
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1988 Akademie-Verlag Berlin
About this paper
Cite this paper
Hansen, H., Löwe, M. (1988). Modular algebraic specifications. In: Grabowski, J., Lescanne, P., Wechler, W. (eds) Algebraic and Logic Programming. ALP 1988. Lecture Notes in Computer Science, vol 343. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-50667-5_69
Download citation
DOI: https://doi.org/10.1007/3-540-50667-5_69
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-50667-6
Online ISBN: 978-3-540-46063-3
eBook Packages: Springer Book Archive