Skip to main content
SpringerLink
Log in

Equational Specification of Partial Higher Order Algebras

  • Conference paper
Logic of Programming and Calculi of Discrete Design

Part of the book series: NATO ASI Series ((NATO ASI F,volume 36))

Abstract

The theory of algebraic abstract types specified by positive conditional formulas formed of equations and a definedness predicate is outlined and extended to hierarchical types with “nonstrict” operations, partial and even infinite objects. Its model theory is based on the concept of partial interpretations. Deduction rules are given, too. Models of types are studied where all explicit equations have solutions. The inclusion of higher order types, i.e. types comprising higher order functions are treated, leads to an algebraic (“equational”) specification of algebras including sorts with “infinite” objects and higher order functions (“functionals”). Finally concepts of implementations of algebraic types are studied.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. J.A. Goguen, J.W. Thatcher, E.G. Wagner, J.B. Wright: Initial algebra semantics and continuous algebras. IBM Research Report RC-5701, November 1975, JACM 24 (1977) 68–95

    Article  MathSciNet  MATH  Google Scholar 

  2. F.L. Bauer et al.: Programming in a wide spectrum language: A collection of examples. SCP 1,(1981) 73–114

    MATH  Google Scholar 

  3. G. Birkhoff, J.D. Lipson: Heterogeneous algebras. J. of Combinatorial Theory 8 (1970) 115–133

    Article  MathSciNet  MATH  Google Scholar 

  4. M. Broy: Algebraic Methods for program construction: The project CIP. In: P. Pepper (ed.): Program Transformation and Programming Environments. Springer 1984, 199 – 222

    Chapter  Google Scholar 

  5. M. Broy: On modularity in programming. In: H. Zemanek (ed.): 25 years of IFIP. North Holland Publ. Company 1986, 347–362

    Google Scholar 

  6. M. Broy, M. Wirsing: On the algebraic extensions of abstract data types. J. Diaz, I. Ramos (eds): International Colloquium on Formalization of Programming Concepts, Peniscola, April 1981, Lecture Notes in Computer Science 107, Berlin-Heidelberg-New York: Springer 1981, 244–251

    Google Scholar 

  7. M. Broy, M. Wirsing: Partial abstract data types. Acta Informatica 18:1, November 1982, 47–64

    Article  MathSciNet  MATH  Google Scholar 

  8. M. Broy, M. Wirsing: Generalized heterogeneous algebras and partial interpretations. In: Proc. CAAP 84. Lecture Notes in Computer Science 159, Berlin-Heidelberg-New York: Springer 1984, 1–34

    Google Scholar 

  9. M. Broy, J.C. Pair, M. Wirsing: A systematic study of models of abstract data types. TCS 33 (1984), 139–174

    Article  MathSciNet  MATH  Google Scholar 

  10. M. Broy, B. Möller, P. Pepper, M. Wirsing: Algebraic implementations preserve program correctness. To appear in Science of Computer Programming

    Google Scholar 

  11. R.M. Burstall, J.A. Goguen: Putting theories together to make specifications. IJCAI 77, 1045–1058

    Google Scholar 

  12. CEP-L. Lecture Notes in Computer Science 183, Springer 1985

    Google Scholar 

  13. H.-D. Ehrich: On the theory of specification, implementation and parameterization of abstract data types. JACM 29:1, 1982

    Article  MathSciNet  Google Scholar 

  14. H.D. Ehrich, U. Lipeck: Proving implementations correct — two alternative approaches. In: Lavington, D. (ed.): MP — Congress 80. Amsterdam: North — Holland, pp. 83–88 (1980)

    Google Scholar 

  15. H. Ehrig, B. Mahr: Fundamentals of algebraic specification 1. Springer 1985

    MATH  Google Scholar 

  16. H. Ehrig, H.-J. Kreowski, B. Mahr, P. Padawitz: Algebraic implementation of abstract data types. TCS 20 (1982) 209–263

    Article  MATH  Google Scholar 

  17. J.A. Goguen, J. W. Thatcher, E.G. Wagner An initial algebra approach to the specification, correctness and implementation of abstract data types. In: Current Trends in Programming Methodology IV: Data 1978

    Google Scholar 

  18. G. Grätzer: Universal algebra. Princeton: Van Nostrand, 1968

    MATH  Google Scholar 

  19. J.V. Guttag, JJ. Horning: The algebraic specification of abstract data types. Acta Informatica 10 (1978) 27–52

    Article  MathSciNet  MATH  Google Scholar 

  20. J.V. Guttag, E. Horowitz, D.R. Musser: Abstract data types and software validation. CACM 21:12(1978)1048–1064

    MathSciNet  MATH  Google Scholar 

  21. C.A.R. Hoare: Proof of correctness of data representation. Acta Informatica 1:4 (1972) 271–281

    Article  MATH  Google Scholar 

  22. G. Huet, D.C. Oppen: Equations and rewrite rules: a survey. In: R. V. Book: Formal Language Theory: Perspectives and Open Problems, Academic Press 1980

    Google Scholar 

  23. H. Hussmann: Unification in conditional-equational theories. Universität Passau, Fakultät für Mathematik und Informatik, Report MIP-8502, 1985

    Google Scholar 

  24. S.C. Kleene: Introduction to metamathematics. New York: Van Nostrand 1952

    MATH  Google Scholar 

  25. A. Laut: Safe procedural implementations of algebraic types. IPL 11:45 (1980) 147–151

    Article  Google Scholar 

  26. B. Liskov, S. Zilles: Specification techniques for data abstraction. IEEE Transactions on Software Engineering 1:1, 7–18 (1975)

    Google Scholar 

  27. Z. Manna: Mathematical theory of computation. New York: McGraw Hill 1974

    MATH  Google Scholar 

  28. B. Möller: Unendliche Objekte und Geflechte. Technische Universität München, Institut für Informatik, TUM-I8213, Ph. D. Thesis 1982

    Google Scholar 

  29. B. Möller: Algebraic specifications with higher order operators. In: L. Meertens (ed.): Proc. MP TC2 Working Conference on Program Specification and Transformation, Bad Tölz, April 1986. Amsterdam: North-Holland (to appear)

    Google Scholar 

  30. D. Parnas: On the criteria being used to decompose modules into systems. CACM 15 (1972) 1053–1058

    Google Scholar 

  31. A. Poigne: Higher order data structures — cartesian closure versus λ-calculus. Proc. STACS 1984, Lecture Notes in Computer Science 166, Berlin-Heidelberg-New York: Springer 1984, 174–185

    Google Scholar 

  32. D. Scott: Outline of a mathematical theory of computation. Proc. 4th Annual Princeton Conference on Information Sciences and Systems 1970,169–176

    Google Scholar 

  33. M. Wirsing, M. Broy: Abstract data types as lattices of finitely generated models. In: Dembinski, P. (ed.): Mathematical Foundations of Computer Science — 9th Symposium, Rydzyna, Poland, Sept. 1–5, 1980. Lecture Notes in Computer Science 88. Berlin-Heidelberg-New York: Springer 1980, 673–685

    Google Scholar 

  34. M. Wirsing, P. Pepper, H. Partsch, W. Dosch, M. Broy: On hierarchies of abstract data types. Acta Informatica 20, 1983, 1–33

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Fakultät für Mathematik und Informatik, Universität Passau, Postfach 2540, D-8390, Passau, Germany

    Manfred Broy

Authors
  1. Manfred Broy
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Fakultät für Mathematik und Informatik, Universität Passau, Postfach 2540, 8390, Passau, Federal Republic of Germany

    Manfred Broy

Rights and permissions

Reprints and permissions

Copyright information

© 1987 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Broy, M. (1987). Equational Specification of Partial Higher Order Algebras. In: Broy, M. (eds) Logic of Programming and Calculi of Discrete Design. NATO ASI Series, vol 36. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-87374-4_8

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-87374-4_8

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-87376-8

  • Online ISBN: 978-3-642-87374-4

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation