Abstract
This paper is devoted to the methodology of using denotational techniques in software design. Since denotations describe the mechanisms of a system and syntax is only a user-visible representation of these mechanisms, we suggest that denotations be developed in the first place and that syntax be derived from them later. That viewpoint is opposite to the traditional (descriptive) style where denotational techniques are used in assigning a meaning to some earlier defined syntax. Our methodology is discussed on an algebraic ground where both denotations and syntax constitute many-sorted algebras and where denotational semantics is a homomorphism between them. On that ground the construction of a denotational model of a software system may be regarded as a derivation of a sequence of algebras. We discuss some mathematical techniques which may support that process especially this part where syntax is derived from denotations. The suggested methodology is illustrated on an example where we develop a toy programming language with rendezvous mechanisms.
Research reported in this paper contributes to project MetaSoft.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
AHO A.V., JOHNSON S.C., ULLMAN J.D. Deterministic parsing of ambiguous grammars, Com. ACM no 8, vol. 18 (1975), 441–452
BJOERNER D., JONES C.B. The Vienna Development Method: The Meta Language, LNCS Vol.61,Springer Verlag 1978
BJOERNER D., JONES C.B. Formal Specification and Software Development, Prentice Hall Int. 1982
BJOERNER D., OEST O.N. (eds.) Towards a Formal Description of ADA, LNCS 98, Springer 1980
BLIKLE A. Proving programs by sets of computations, MFCS Proc. Symp. Warsaw-Jadwisin 1974, LNCS 28, Springer 1975, 313–358
BLIKLE A. Noninitial algebraic semantics, Proc. conf. Nyborg 1984, to be published by North Holland
BLIKLE A. Denotational constructors, a manuscript 1986
BLIKLE A., TARLECKI A. Naive denotational semantics, in: Information Processing 83 (Proc. IFIP Congress 1983, R.E.A.Manson ed.), North Holland 1983
BROOKES S.D., HOARE C.A.R., ROSCOE A.W. A theory of communicating sequential processes, J.ACM 31 (1984), 560–599
COHN P.M. Universal Algebra, D.Reidel Publishing Company 1981
DERSHOWITZ N. Computing with rewrite systems, Information and Control 65 (1985), 122–157
EHRIG H., MAHR B. Fundamentals of Algebraic Specification 1, Springer 1985
GOGUEN J.A. Abstract errors for abstract data types, in: Formal Description of Programming Concepts (Proc. IFIP TC-2 Working Conf. 1977, ed. E.Neuhold), North-Holland 1978
GOGUEN J., MESEGUER J., PLAISTED D. Programming with perameterized abstract objects in OBJ, in: Theory and Practice of Software Technology, North Holland 1983, 163–194
GOGUEN J.A., THATCHER J.W., WAGNER E.G., WRIGHT J.B. Initial algebra semantics and continuous algebras, J. ACM 24 (1974), 68–95
GORDON M.J.C. The Denotational Description of Programming Languages, Springer 1979
HARRISON M.A. Introduction to Formal Language Theory, Addison-Wesley Publishing Company 1978
HOARE C.A.R. Communicating Sequential Processes, Prentice Hall Int.1985
INMOS Ltd. OCCAM™ Programming Manual, Prentice-Hall Int. 1984
MAGGIOLO-SCHETTINI A., WINKOWSKI J. An algebra of processes, Journal of Computer and System Science, to appear
MAZURKIEWICZ A. Recursive algorithms and formal languages, Bull. Acad. Polon. Sci., Sér. Sci. Math. Astronom. et Phys. 20 (1972), 799–803
MAZURKIEWICZ A. Semantics of concurrent systems: a modular fixed-point trace approach, Advances in Petri Nets 1984 (G.Rozenberg ed.), LNCS 188, Springer 1984, 352–371
MESEGUER J., GOGUEN A.J. Initiality, induction and computability, in: Application of Algebra to Language Definition and Compilation, (M.Nivat, J.Reynolds eds.), Cambridge Univ. Press 1985, 459–541
MOSSES P. The mathematical semantics of Algol 60, Technical Monograph PRG-12, Oxford University 1974
MCCARTHY J. A basis for a mathematical theory of computation, Western Joint Computer Conf. 1961, since then published in Computer Programming and Formal Systems (P. Braffort, D. Hirschberg eds.), North-Holland, Amstardam 1967, 33–70
SCOTT D., STRACHEY Ch. Toward a mathematical semantics for computer languages, Technical Monograph PRG-6, Oxford University 1971
STOY J.E. Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory, The MIT Press, Cambridge Mass. 1977
TENNENT R.D. The denotational semantics of programming languages, Communication of ACM, Vol.19 (1976), 437–453
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1987 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Blikle, A. (1987). Denotational engineering or from denotations to syntax. In: Bjørner, D., Jones, C.B., Mac an Airchinnigh, M., Neuhold, E.J. (eds) VDM '87 VDM — A Formal Method at Work. VDM 1987. Lecture Notes in Computer Science, vol 252. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-17654-3_12
Download citation
DOI: https://doi.org/10.1007/3-540-17654-3_12
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-17654-1
Online ISBN: 978-3-540-47740-2
eBook Packages: Springer Book Archive