Abstract
Parameterized specifications of abstract data type are studied within the theory of algebraic specifications. In the algebraic theory as introduced by the ADJ-group a parameterized specification, like set (data), consists of a parameter declaration data and a target specification set (data). This basic algebraic approach is combined with a very general notion of requirements which have to be satisfied for the parameters of the specification. Especially we can use fixed basic types like bool or nat in the parameter part, a feature which is already included in the algebraic specification language CLEAR. This allows to specify bounded types like bounded natural numbers nat (bound) with variable bound or bounded arrays. Moreover the requirement feature allows to use arbitrary predicate formulas which are also used in logical requirement specifications for software systems. In spite of this generality the theory developed for the basic algebraic approach can be fully extended to the case with requirements. The basic result is an extension lemma which allows to show correctness of parameter passing and associativity of nested parameterized specifications like set (stack (nat)). Correctness of such composite specifications is automatically induced by correctness of the parts.
This theory with requirements is still based on initial algebra semantics but with slight modifications it can also be used for final algebraic semantics.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
(JAG,JWT,EGW): An initial algebra approach to the specification, correctness, and implementation of abstract data types, IBM Research Report RC-6487, Oct 1976. Current Trends in Programming Methodology, IV: Data Structuring (R.T. Yeh, Ed.) Prentice Hall, New Jersey (1978), pp. 80–149
(JWT,EGW,JBW) J.W. Thatcher, E.G.Wagner, J.B. Wright: Data Type Specification: parameterization and the power of specification techniques, Proc. SIGACT 10th Annual Symp. on Theory of Computing, May 1978, pp. 119–132, revised version in IBM Research Report RC-7757 (1979)
(HE,HJK,JWT,EGW,JBW) H. Ehrig, H.-J. Kreowski, J.W. Thatcher, E.G. Wagner, J.B. Wright: Parameterized data types in algebraic specification languages, Proc. 7th ICALP Nordwijkerhout, July 1980: Lect. Not. in Comp. Sci. (1980), pp. 157–168
(HE,HJK,JWT,EGW,JBW) H. Ehrig, H.-J. Kreowski, J.W. Thatcher, E.G. Wagner, J.B. Wright: Parameter passing in algebraic specification languages, Draft Version, TU Berlin, March 1980
Arbib, M.A., Manes, E.G.: Arrows, Structures and Functors: The categorical imperative, Academic Press, New York, 1975
Burstall, R.M., Goguen, J.A.: Putting Theories together to make Specifications, Proc. 1977 IJCAI, MIT, Cambridge, MA, Aug. 1977
Burstall, R.M., Goguen, J.A.: The Semantics of CLEAR, a Specification Language, Proc. 1979 Copenhagen Winter School on Abstract Software Specifications (1980)
Ehrich, H.-D.: On the theory of specification, implementation and parameterization of abstract data types, Research Report, Dortmund 1978
Ehrich, H.-D., Lohberger, V.G.: Constructing Specifications of Abstract Data Types by Replacements, Proc. Int. Workshop Graph Grammars and Appl. Comp. Sci. and Biology, Bad Honnef 1978, Lect. Not. in Comp. Sci. 73 (1979), pp. 180–191
Ehrig, H., Kreowski, H.-J., Padawitz, P.: Stepwise specification and implementation of abstract data types: Technical University of Berlin, Report, Nov. 1977. Proc. 5th ICALP, Udine, July 1978: Lect. Not. in Comp. Sci. 62 (1978), pp. 205–226
—: Algebraic Implementation of Abstract Data Types: Concept, Syntax, Semantics, Correctness; Proc. 7th ICALP, Nordwijkerhout, July 1980, Lect. Not. in Comp. Sci. (1980)
Floyd, Ch.: Proc. 2nd German Chapter of The ACM-Meeting "Software Engineering — Entwurf und Spezifikation" (editor), Teubner Verlag 1981
Ganzinger, H.: Parameterized Specifications: Parameter Passing and Implementation, version Sept.1980, to appear in TOPLAS
—: A Final Algebra Semantics for Parameterized Specifications, Draft Version, UC Berkeley, November 1980
Hornung, G., Raulefs, P.: Initial and Terminal Algebra Semantics of Parameterized Abstract Data Type Specification with Inequalities (this volume)
Hupbach, U.L.: Abstract Implementation and Parameter Substitution, submitted to 3rd Hungarian Comp. Sci. Conf., Budapest 1981
Jenks, R.D.: MODLISP: An Introduction, Lect. Not. in Comp. Sci. 72 (1979), pp. 466–480, new version in preparation
Klaeren, H.A.: On Parameterized Abstract Software Modules using Inductively Specified Operations, Research Report TH Aachen Nr.66, (1980)
Kreowski, H.-J.: Algebra für Informatiker; LV-Skript WS 78/79, FB 20, TU Berlin (1978)
Reichel, H.: Initially Restricting Algebraic Theories, Proc. MFCS'80, Rydzyna, Sept. 1980, Lect. Not. in Comp. Sci. 88 (1980), pp. 504–514
Wirsing, M., Broy M.: Abstract Data Types as Lattices of Finitely Generated Models, Proc. MFCS'80, Rydzyna, Sept. 1980, Lect. Not. in Comp. Sci. 88 (1980), pp. 673–685
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1981 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ehrig, H. (1981). Algebraic theory of parameterized specifications with requirements. In: Astesiano, E., Böhm, C. (eds) CAAP '81. CAAP 1981. Lecture Notes in Computer Science, vol 112. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-10828-9_51
Download citation
DOI: https://doi.org/10.1007/3-540-10828-9_51
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-10828-3
Online ISBN: 978-3-540-38716-9
eBook Packages: Springer Book Archive