Algebraic specifications with generating constraints
- 112 Downloads
In this paper we take a new look at one of the basic principles of abstract data types. Due to this principle the domain of an abstract data type must be generated by the operations. In the initial algebraic approach as well as in the loose case with initial restrictions or data constraints this principle is satisfied because of initiality resp. free construction. Actually initiality makes sure that the data under consideration are not only generated but even freely generated by the operations. In this paper we do not consider free generation but only generation leading to the new concept of algebraic specifications with generating constraints.
This new look was also motivated by the notion of hierarchy constraints, introduced by the CIP-group in Munich, but there are two main differences between hierarchy and generating constraints: First of all we remove the consistency condition “TRUE≠FALSE” for bool. This part of hierarchy constraints can be expressed (if necessary) in the axiom part of the specifications. Secondly we give a mechanism how to construct generating constraints and how to translate or reflect them from one part of a specification to other parts. More precisely we define syntax and semantics of a language building up generating constraints together with the stepwise construction of an algebraic specification. The main result of this paper shows how an arbitrary generating constraint built up in this way can be transformed to a very simple constraint in canonical form which is equivalent to the given one. Equivalence of two generating constraints on the same algebraic specification means that they have the same semantics, i.e. they define the same class of algebras.
Finally we discuss how concepts and results of this paper could be used for the design of algebraic specification languages where not only the specifications but also the constraints are built up in a stepwise way.
KeywordsForgetful Functor Data Constraint Denotational Semantic Constraint Language Abstract Data Type
Unable to display preview. Download preview PDF.
- /ADJ 76-78/.Goguen, J.A., Thatcher, J.W., Wagner, E.G.: An initial algebra approach to the specification, correctness, and implementation of abstract data types, IBM Research Report RC-6487, Oct. 76, Current Trends in Progr. Method., IV: Data Structuring (R.T. Yeh, Ed.) Prentice Hall, New Jersey (1978), 80–149Google Scholar
- /ADJ 77/.-, Wright, J.B.: Initial algebra semantics and continous algebras, J.ACM 24, 68–95 (1977)Google Scholar
- /ADJ 78/.Thatcher, J.W., Wagner, E.G., Wright, J.B.: More on advice on structuring compilers and proving them correct, TCS 15 (1981), 223–249Google Scholar
- /ADJ 81/.Ehrig, H., Kreowski, H.-J., Thatcher, J.W., Wagner, E.G., Wright, J.B.: Parameter Passing in Algebraic Specification Languages, Proc. Aarhus Workshop on Prog. Spec., 1981, LNCS 134 (1982), 322–369Google Scholar
- /BDPPW 79/.Broy, M., Dorsch, N., Partsch, H., Pepper, P., Wirsing, M.: Existential quantifiers in abstract data types; Proc. 6th ICALP, LNCS 71, 73–87 (1979)Google Scholar
- /BG 80/.Burstall, R., Goguen, J.: The semantics of CLEAR, a Specification Language, Proc. Advanced Course on Abstr. Software Spec., LNCS 86 (1980), 294–332Google Scholar
- /BW 82/.Bloom, S.L., Wagner, E.G.: Many sorted theories and their algebras, with examples from Comp. Sci. (working paper), IBM Research Center, 1982Google Scholar
- /Ehr 82/.Ehrich, H.-D.: On the theory of specification, implementation and parameterization of abstract data types, J. ACM 29, No.1 (1982), 206–227Google Scholar
- /Ehr 81/.Ehrig, H.: Parameterized Specifications with Requirements, Proc. CAAP'81, LNCS 112 (1981), 1–24Google Scholar
- /EFH 83/.Ehrig, H., Fey, W., Hansen, H.: ACT ONE: An Algebraic Specification Language with Two Levels of Semantics, Techn. Report TU Berlin, No. 83-03, 1983Google Scholar
- /EKP 80/.Ehrig, H., Kreowski, H.-J., Padawitz, P.: Algebraic Implementation of Abstract Data Types: Concept, Syntax, Semantics and Correctness, Proc. 7th ICALP, LNCS 85 (1980), 142–156; long version to appear in TCSGoogle Scholar
- /EK 82/.Ehrig, H., Kreowski, H.-J.: Parameter Passing Commutes with Implementation of Parameterized Data Types, Proc. 9th ICALP, LNCS 140 (1982), 197–211Google Scholar
- /ETLZ 82/.Ehrig, H., Thatcher, J., Lucas, P., Zilles, S.: Denotational and initial algebra semantics of the algebraic specification language LOOK (draft paper), IBM Research Center (1982)Google Scholar
- /EWT 82/.Ehrig, H., Wagner, E.G., Thatcher, J.W.: Algebraic Constraints for Specifications and Canonical Form Results, Techn.Report TU Berlin, No. 82-09, 1982Google Scholar
- /Gut 75/.Guttag, J.V.: The specification and application to programming of abstract data types, Univ. Toronto, Techn.Report CSRG-59, (1975)Google Scholar
- /HKR 80/.Hupbach, U.L., Kaphengst, M., Reichel, H.: Initial algebraic specifications of data types, parameterized data types and algorithms, VEB Robotron ZFT, Techn. Report, Dresden, 1980Google Scholar
- /Lip 82/.Lipeck, U.: Ein algebraischer Kalkül für einen strukturierten Entwurf von Datenabstraktionen, PhD Thesis, Univ. Dortmund, 1982Google Scholar
- /LZ 75/.Liskov, B.H., Zilles, S.N.: Specification Techniques for Data Abstraction, IEEE Trans.on Soft.Eng., Vol.SE-1, No.1 (1975),7–19Google Scholar
- /SW 82/.Sanella, D., Wirsing, M.: Implementation of parameterized specifications, Proc. 9th ICALP, LNCS 140 (1982), 473–488Google Scholar
- /WEB 82/.Wagner, E.G., Ehrig, H., Bloom, S.: Parameterized data types, parameter passing and canonical constraints (working paper) IBM Research Center (1982)Google Scholar
- /Zil 74/.Zilles, S.N.: Algebraic specifications of data types, Project MAC Prog. Rep. 11, MIT (1974), 52–58Google Scholar
- /ZLT 82/.Zilles, S.N., Lucas, P., Thatcher, J.W.: A look at algebraic specifications, IBM Research Report RJ 3568, 1982Google Scholar