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.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Bjorner, D. and Jones, C. B.; The Vienna Development Method. Lecture Notes in Computer Science 61, 1978.
Burstall, R. M. and Goguen, J. A.; Putting Theories Together to Make Specifications. Proc. 5th Int. Joint Confr. on Artificial Intelligence, 1977.
Burstall, R. M., and Goguen, J. A.; The Semantics of CLEAR, a Specification Language. Lecture Notes in Computer Science 86, 1980.
Constable, R. L. and Donahue, J. E.; A Hierarchical Approach to Formal Semantics. ACM TOPLAS 1(1), 1979.
Goguen, J. A. and Tardo, J.; An Introduction to OBJ-T. Specification of Reliable Software, IEEE, Cambridge Mass., April 1979.
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.
Goguen, J. A.; Semantics of Computation. Lecture Notes in Computer Science 25, 1975.
Goguen, J. A.; Abstract Errors for Abstract Data Types. Working Conference on Formal Description of Programming Concepts. IFIP, 1977.
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.
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.
Gordon, M.; The Denotational Description of Programming Languages. Springer-Verlag, 1979.
Jones, C. B.; Models of Programming Language Concepts. Lecture Notes in Computer Science 81, 1980.
Landin, P. J.; The Next 700 Programming Languages. Communications of the ACM 9, 1966.
McCarthy, J.; Towards a Mathematical Science of Computation. Proc. 1962 IFIP Congress, North-Holland, 1962.
Mosses, P.; SIS, a Compiler-Generator System using Denotational Semantics. Technical Report, Aarhus University, Department of Computer Science, 1978.
Mosses, P.; Modular Denotational Semantics. Technical Report, Aarhus University, Computer Science Department, Aarhus, Denmark, 1979.
Musser, D.; On Proving Inductive Properties of Abstract Data Types. Proc. 7th ACM Symp. on Principles of Programming Languages, 1980.
Pagan, F. G.; Algol 68 as a Metalanguage for Denotational Semantics. Computer Journal 22, 1979.
Parsaye-Ghomi, K.; Higher Order Data Types. PhD Thesis, Computer Science Department, UCLA, 1981.
Raoult, J-C. and Vuillemin, J.; Operational and Semantic Equivalence between Recursive Programs. Journal of the ACM 27(4), 1980.
Reynolds, J. C.; GEDANKEN, a Simple Typeless Language Based on the Reference Concept. Communications of the ACM 13(5), 1970.
Scott, D.; Data Types as Lattices. SIAM Journal of Computing 5(3), 1976.
Tennent, R. D.; The Denotational Semantics of Programming Languages. Communications of the ACM 19(8), 1976.
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.
Author information
Authors and Affiliations
Editor information
Rights 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