Advertisement

Algebraic specifications with generating constraints

  • H. Ehrig
  • E. G. Wagner
  • J. W. Thatcher
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 154)

Abstract

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.

Keywords

Forgetful Functor Data Constraint Denotational Semantic Constraint Language Abstract Data Type 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. /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
  2. /ADJ 77/.
    -, Wright, J.B.: Initial algebra semantics and continous algebras, J.ACM 24, 68–95 (1977)Google Scholar
  3. /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
  4. /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
  5. /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
  6. /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
  7. /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
  8. /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
  9. /Ehr 81/.
    Ehrig, H.: Parameterized Specifications with Requirements, Proc. CAAP'81, LNCS 112 (1981), 1–24Google Scholar
  10. /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
  11. /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
  12. /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
  13. /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
  14. /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
  15. /Gut 75/.
    Guttag, J.V.: The specification and application to programming of abstract data types, Univ. Toronto, Techn.Report CSRG-59, (1975)Google Scholar
  16. /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
  17. /Lip 82/.
    Lipeck, U.: Ein algebraischer Kalkül für einen strukturierten Entwurf von Datenabstraktionen, PhD Thesis, Univ. Dortmund, 1982Google Scholar
  18. /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
  19. /SW 82/.
    Sanella, D., Wirsing, M.: Implementation of parameterized specifications, Proc. 9th ICALP, LNCS 140 (1982), 473–488Google Scholar
  20. /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
  21. /Zil 74/.
    Zilles, S.N.: Algebraic specifications of data types, Project MAC Prog. Rep. 11, MIT (1974), 52–58Google Scholar
  22. /ZLT 82/.
    Zilles, S.N., Lucas, P., Thatcher, J.W.: A look at algebraic specifications, IBM Research Report RJ 3568, 1982Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1983

Authors and Affiliations

  • H. Ehrig
    • 1
  • E. G. Wagner
    • 2
  • J. W. Thatcher
    • 2
  1. 1.Technische UniversitätBerlinGermany
  2. 2.IBM T.J.W. Research CenterYorktown HeightsUSA

Personalised recommendations