Skip to main content

Algebraic denotational semantics using parameterized abstract modules

  • Communications
  • Conference paper
  • First Online:
Formalization of Programming Concepts (ICFPC 1981)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 107))

Included in the following conference series:

Abstract

This paper describes a method for giving structured algebraic denotational definitions of programming language semantics. The basic idea is to use parameterized abstract data types to construct a directed acyclic graph of modules, such that each module corresponds to some feature of the language. A "feature" in this sense is sometimes a syntactic construction, and is sometimes a more basic language design decision. Our definitions are written in the executable algebraic specification language OBJT. Among the advantages of our approach are the following: it is relatively easier to understand the definitions because they are organized into modules and use flexible user-definable syntax; it is also relatively easy to modify or to extend the definitions, not only because of the modularity, but also because of the use of parameterization; it is possible to debug the definitions by executing test cases, which in this case are programs; the definitions are relatively compact; and they impose relatively little implementation bias. This paper illustrates these points with the definition of a modest programming language with integer and boolean expressions, blocks, iteration, conditional, input and output, and side-effect-only procedures, which can be assigned to variables and passed as parameters.

Work supported in part by Office of Naval Research, Contract N00014-80-C-0296 and National Science Foundation, Contract 4-442510-21723.

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

Access this chapter

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Bjorner, D. and Jones, C. B.; The Vienna Development Method. Lecture Notes in Computer Science 61, 1978.

    Google Scholar 

  2. Burstall, R. M. and Goguen, J. A.; Putting Theories Together to Make Specifications. Proc. 5th Int. Joint Confr. on Artificial Intelligence, 1977.

    Google Scholar 

  3. Burstall, R. M., and Goguen, J. A.; The Semantics of CLEAR, a Specification Language. Lecture Notes in Computer Science 86, 1980.

    Google Scholar 

  4. Constable, R. L. and Donahue, J. E.; A Hierarchical Approach to Formal Semantics. ACM TOPLAS 1(1), 1979.

    Google Scholar 

  5. Goguen, J. A. and Tardo, J.; An Introduction to OBJ-T. Specification of Reliable Software, IEEE, Cambridge Mass., April 1979.

    Google Scholar 

  6. Goguen, J. A., Thatcher, J. W., Wagner, E. and Wright, J. B.; Initial Algebra Semantics and Continuous Algebras. Journal of the ACM 24(1), 1977.

    Google Scholar 

  7. Goguen, J. A.; Semantics of Computation. Lecture Notes in Computer Science 25, 1975.

    Google Scholar 

  8. Goguen, J. A.; Abstract Errors for Abstract Data Types. Working Conference on Formal Description of Programming Concepts. IFIP, 1977.

    Google Scholar 

  9. Goguen, J. A.; Order Sorted Algebras. UCLA Semantics and Theory of Computation Report No. 14, 1978; to appear in Journal of Computer and System Science.

    Google Scholar 

  10. Goguen, J. A.; How to Prove Algebraic Inductive Hypotheses without Induction: with applications to the correctness of data type representations. Lecture Notes in Computer Science 87, 1980.

    Google Scholar 

  11. Gordon, M.; The Denotational Description of Programming Languages. Springer-Verlag, 1979.

    Google Scholar 

  12. Jones, C. B.; Models of Programming Language Concepts. Lecture Notes in Computer Science 81, 1980.

    Google Scholar 

  13. Landin, P. J.; The Next 700 Programming Languages. Communications of the ACM 9, 1966.

    Google Scholar 

  14. McCarthy, J.; Towards a Mathematical Science of Computation. Proc. 1962 IFIP Congress, North-Holland, 1962.

    Google Scholar 

  15. Mosses, P.; SIS, a Compiler-Generator System using Denotational Semantics. Technical Report, Aarhus University, Department of Computer Science, 1978.

    Google Scholar 

  16. Mosses, P.; Modular Denotational Semantics. Technical Report, Aarhus University, Computer Science Department, Aarhus, Denmark, 1979.

    Google Scholar 

  17. Musser, D.; On Proving Inductive Properties of Abstract Data Types. Proc. 7th ACM Symp. on Principles of Programming Languages, 1980.

    Google Scholar 

  18. Pagan, F. G.; Algol 68 as a Metalanguage for Denotational Semantics. Computer Journal 22, 1979.

    Google Scholar 

  19. Parsaye-Ghomi, K.; Higher Order Data Types. PhD Thesis, Computer Science Department, UCLA, 1981.

    Google Scholar 

  20. Raoult, J-C. and Vuillemin, J.; Operational and Semantic Equivalence between Recursive Programs. Journal of the ACM 27(4), 1980.

    Google Scholar 

  21. Reynolds, J. C.; GEDANKEN, a Simple Typeless Language Based on the Reference Concept. Communications of the ACM 13(5), 1970.

    Google Scholar 

  22. Scott, D.; Data Types as Lattices. SIAM Journal of Computing 5(3), 1976.

    Google Scholar 

  23. Tennent, R. D.; The Denotational Semantics of Programming Languages. Communications of the ACM 19(8), 1976.

    Google Scholar 

  24. Wand, M.; First-Order Identities as a Defining Language. Technical Report 29 (revised), Computer Science Dept., Indiana University, 1977. Revised version published in Acta Informatica, vol. 14, 1980.

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

J. Díaz I. Ramos

Rights and permissions

Reprints and permissions

Copyright information

© 1981 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Goguen, J.A., Parsaye-Ghomi, K. (1981). Algebraic denotational semantics using parameterized abstract modules. In: Díaz, J., Ramos, I. (eds) Formalization of Programming Concepts. ICFPC 1981. Lecture Notes in Computer Science, vol 107. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-10699-5_106

Download citation

  • DOI: https://doi.org/10.1007/3-540-10699-5_106

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-10699-9

  • Online ISBN: 978-3-540-38654-4

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics