Advertisement

Unifying initial and loose semantics of parameterized specifications in an arbitrary institution

  • Hubert Baumeister
CAAP Colloquium On Trees In Algebra And Programming
Part of the Lecture Notes in Computer Science book series (LNCS, volume 493)

Abstract

In this paper we are going to present a theory of parameterized abstract datatypes as the model-theoretic level of parameterized specifications. We will show that parameterized abstract datatypes allow us to model the main approaches to the semantics of parameterized specifications, the loose approach (e.g. [GB90]) and the free functor semantics (e.g. [TWW82, EM85]), using the same formalism. As a consequence we obtain that, when using data constraints [Rei86, GB90, OSC89, EM90] in a specification language, this language is able to cope with both the loose and the free functor semantics at the same time. To be independent of a specific logic this theory is developed in the context of an arbitrary institution.

Keywords

Parameterized Specification Full Subcategory Initial Object Forgetful Functor Equational Logic 
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.

References

  1. [Bau90]
    Hubert Baumeister. Über die Stabilität parameterisierter algebraischer Spezifikationen (About the stability of parameterized algebraic specifications). Master's thesis, Universität Dortmund, July 1990.Google Scholar
  2. [BG80]
    R.M. Burstall and J.A. Goguen. The semantics of Clear, a specification language, February 1980.Google Scholar
  3. [Cla87]
    Ingo Claßen. Revised ACT ONE: Categorical constructions for an algebraic specification language. In H. Ehrig, H. Herrlich, J.-J. Kreowski, and G. Preuß, editors, Categorical Methods in Computer Science with Aspects from Topology, number 393 in LNCS, pages 124–141. Springer, 1987.Google Scholar
  4. [EGL89]
    Hans-Dieter Ehrich, Martin Gogolla, and Udo Walter Lipeck. Algebraische Spezifikation abstrakter Datentypen (Algebraic Specification of Abstract Datatypes). B. G. Teubner Stuttgart, 1989.Google Scholar
  5. [Ehr89]
    Hartmut Ehrig. A categorical concept of constraints for algebraic specifications. In H. Ehrig, H. Herrlich, H.-J. Kreowski, and G. Preuß, editors, Categorical Methods in Computer Science, number 393 in LNCS. Springer Verlag, 1989.Google Scholar
  6. [EM85]
    Hartmut Ehrig and Bernd Mahr. Fundamentals of Algebraic Specification 1: Equations and initial Semantics, volume 6 of EATCS Monographs on Theoretical Computer Science. Springer, 1985.Google Scholar
  7. [EM90]
    Hartmut Ehrig and Bernd Mahr. Fundamentals of Algebraic Specification 2: Module Specifications and Constraints, volume 21 of EATCS Monographs on Theoretical Computer Science. Springer, 1990.Google Scholar
  8. [EPO89]
    H. Ehrig, P. Pepper, and F. Orejas. On recent trends in algebraic specification. In ICALP 89, pages 263–288, 1989.Google Scholar
  9. [GB90]
    J. A. Goguen and R. Burstall. INSTITUTIONS: Abstract model theory for specification and programming, 1990.Google Scholar
  10. [GTW76]
    J.A. Goguen, J.W. Thatcher, and E.G. Wagner. An initial algebra approach to the specification, correctness and implementation of abstract data types, 1976.Google Scholar
  11. [Kre89]
    Hans-Jörg Kreowski. Colimits as parameterized data types. In H. Ehrig, H. Herrlich, H.-J. Kreowski, and G. Preuß, editors, Categorical methods in Computer Science with aspects from Topology, pages 36–49. Springer, 1989.Google Scholar
  12. [Lip82]
    Udo Lipeck. Ein algebraischer Kalkül für einen strukturierten Entwurf von Datenabstraktionen (An Algebraic Calculus for a Structured Design of Data Abstraction). PhD thesis, Universität Dortmund, 1982.Google Scholar
  13. [Mac88]
    Saunders Mac Lane. Categories for the working mathematician. Graduated Texts in Mathematics. Springer, fourth edition, 1988.Google Scholar
  14. [OSC89]
    F. Orejas, V. Sacristán, and S. Clerici. Development of algebraic specifications with constraints. In H. Ehrig, H. Herrlich, H.-J. Kreowski, and G. Preuß, editors, Categorical methods in Computer Science with aspects from Topology, pages 36–49. Springer, 1989.Google Scholar
  15. [Poi89]
    Axel Poigné. Foundations are rich institutions, but institutions are poor foundations. In H. Ehrig, H. Herrlich, H.-J. Kreowski, and G. Preuß, editors, Categorical methods in Computer Science with aspects from Topology, pages 82–101. Springer, 1989.Google Scholar
  16. [Rei86]
    H. Reichel. Software specification by behavioural canons. TU Magdeburg, 1986.Google Scholar
  17. [Sch86]
    Oliver Schoett. Data Abstraction and the Correctness of Modular Programming. PhD thesis, University of Edinburgh, 1986.Google Scholar
  18. [SST90]
    Donald Sannella, Stefan Sokolowski, and Andrzej Tarlecki. Toward formal development of programs from algebraic specifications: parameterization revisited, 1990.Google Scholar
  19. [ST84]
    Donald Sannella and Andrzej Tarlecki. On observational equivalence and algebraic specification. Technical Report CSR-172-84, University of Edinburgh, 1984.Google Scholar
  20. [ST85]
    Donald Sannella and Andrzej Tarlecki. Specifications in an arbitrary institution. Draft 1, March 1985.Google Scholar
  21. [ST88]
    Donald Sannella and Andrzej Tarlecki. Toward formal development of ML programs: Foundations and methodology. draft (short version), September 1988.Google Scholar
  22. [SW83]
    Donald Sannella and Martin Wirsing. A kernel language for algebraic specification. Internal Report CSR-131-83, University of Edinburgh, September 1983.Google Scholar
  23. [TWW82]
    J. W. Thatcher, E. G. Wagner, and J. B. Wright. Data type specification: Parameterization and the power of specification techniques. acm Transactions on Programming Languages and Systems, 4(4):711–732, October 1982.Google Scholar
  24. [WE85]
    E. G. Wagner and H. Ehrig. Canonical constraints for parameterized data types. Research Report RC 11248 (50666), IBM Thomas J. Watson Research Center, Yorktown Heights, New York 10598 / USA, Jul 1985.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1991

Authors and Affiliations

  • Hubert Baumeister
    • 1
  1. 1.Informatik VUniversität DortmundDortmund-50Germany

Personalised recommendations