article

Open access

Detecting global variables in denotational specifications

Editor: Susan L. Graham Author:

David A. SchmidtAuthors Info & Claims

ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 7, Issue 2

Pages 299 - 310

https://doi.org/10.1145/3318.3323

Published: 01 April 1985 Publication History

PDF eReader

Abstract

Sufficient criteria are given for replacing all occurrences of the store argument in a Scott-Strachey denotational definition of a programming language by a single global variable. The criteria and transformation are useful for transforming denotational definitions into compilers and interpreters for imperative machines, for optimizing applicative programs, and for judging the suitability of semantic notations for describing imperative languages. An example transformation of a semantics of a repeat-loop language to one which uses a global store variable is given to illustrate the technique.

References

[1]

BJ~RNER, D. Rigorous development of interpreters and compilers. In D. Bj~rner and C. Jones (Eds.), Formal Specification and Software Development. Prentice-Hall, Englewood Cliffs, N.J., 1982, pp. 271-320.

Google Scholar

[2]

CURRY, H. B., AND FEYS, R. Cornbinatory Logic, Vol. 1. Elsevier North-Holland, New York, 1958.

Google Scholar

[3]

GOGUEN, J., AND PARSAYE-GHOMI, g. Algebraic denotational semantics using parameterized abstract modules. In Lecture Notes in Computer Science 107: Colloquium on Formalization of Programming Concepts (Pensicola, Spain). Springer-Verlag, New York, 1981, pp. 292-309.

Crossref

Google Scholar

[4]

HOARE, C. A.R. Proof of correctness of data representations. Acta Inf. I (1972), 271-281.

Google Scholar

[5]

HUET, G., AND OPPEN, D. Equations and rewrite rules: A survey. In R. Book (Ed.), Formal Language Theory: Perspectives and Open Problems. Academic Press, New York, 1980, pp. 349- 405.

Google Scholar

[6]

JONES, C.B. The meta language. In D. Bjzrner and C. Jones (Eds.), Formal Specification and Software Development. Prentice-Hall, Englewood Cliffs, N.J., 1982, pp. 271-320.

Google Scholar

[7]

JONES, N. D. (Ed.) Lecture Notes in Computer Science 94: Semantics Directed Compiler Generation. Springer-Verlag, New York, 1980.

Crossref

Google Scholar

[8]

JONES, N. D., MUCHNICK, S. S., AND SCHMWT, D.A. A universal compiler. Tech. Rep. DAIMI IR-17, Computer Science Dept., Univ. Aarhus, Denmark, 1979.

Google Scholar

[9]

MOSSES, P.D. Making denotational semantics less concrete. Presented at the workshop on semantics of programming languages, Bad Honnef, Germany, 1977.

Google Scholar

[10]

MOSSES, P.D. SIS--Reference manual and user's guide. Tech. Rep. DAIMI MD-30, Computer Science Dep., Univ. Aarhus, Denmark, 1979.

Google Scholar

[11]

MOSSES, P.D. A constructive approach to compiler correctness. In N. D. Jones (Ed.) Lecture Notes in Computer Science 94: Semantics Directed Compiler Generation. Springer-Verlag, New York, 1980, pp. 189-210.

Crossref

Google Scholar

[12]

MOSSES, P.D. A semantic algebra for binding constructs. In Lecture notes in Computer Science 107: Formalization of Programming Concepts (Pensicola, Spain). Springer-Verlag, New York, 1981.

Crossref

Google Scholar

[13]

MOSSES, P.D. Abstract semantic algebras! In Formal Description of Programming Concepts II. Elsevier North-Holland, New York, 1983.

Google Scholar

[14]

MYCROFT, A. Abstract interpretation and optimizing transformations for applicative programs. Ph.D. Dissertation, Computer Science Dep., Univ. Edinburgh, Scotland, 1981.

Google Scholar

[15]

O'DONNELL, M. Lecture Notes in Computer Science 58: Computing in Systems Described by Equations. Springer-Verlag, New York, 1977.

Crossref

Google Scholar

[16]

PLOTKIN, G. LCF considered as a programming language. Theor. Comput. Sci. 5(1977), 223- 255.

Google Scholar

[17]

PLOTKIN, G. The category of complete partial orders. In Proceedings, Summer School on Foundations of Artificial Intelligence and Computer Science (Institute di Scienze dell' Informazione, Universita di Pisa), 1978.

Google Scholar

[18]

RAOULT, J.-C., AND SETHI, R. Properties of a notation for combining functions. In Lecture Notes in Computer Science 140: Ninth Colloquium on Automata, Languages, and Programming (Aarhus, Denmark). Springer-Verlag, New York, 1982, pp. 429-441.

Crossref

Google Scholar

[19]

RAOULT, J.-C., AND SETm, R. The global storage needs of a subcomputation. In Proceedings of the 11th ACM Syrup. Principles of Programming Languages (Salt Lake City, Utah, 1984), pp. 148-157.

Crossref

Google Scholar

[20]

REYNOLDS, J.C. Definitional interpreters for higher order programming languages. In Proceedings of the 25th ACM Nat. Conf., (Boston, 1972), pp. 717-740.

Crossref

Google Scholar

[21]

SCHMIDT, D.A. Denotational semantics as a programming language. Internal Rep. CSR-100, Computer Science Dep., Univ. Edinburgh, Scotland, 1982.

Google Scholar

[22]

SCHMIOT, D. A. Detecting global variables in denotational specifications (extended version). Tech. Rep. 84-3, Computer Science Dep., Iowa State Univ., Ames, Iowa, 1984.

Google Scholar

[23]

STOY, J. Denotational Semantics. MIT Press, Cambridge, Mass., 1977.

Google Scholar

[24]

WAND, M. First order identities as a defining language. Acta Inf. 14(1980), 337-357.

Google Scholar

[25]

WAND, M. Semantics-directed computer architecture. In Proceedings of the 9th ACM Syrup. Principles of Programming Languages (Albuquerque, N. Mex., 1982), pp. 234-241.

Crossref

Google Scholar

[26]

WAND, M. Deriving target code as a representation of continuation semantics. ACM Trans. Prog. Lang. Syst. 4(1982), 496-517.

Crossref

Google Scholar

[27]

WEONER, P. Programming language semantics. In R. Rustin (Ed.), Formal Semantics of Programming Languages. Prentice-Hall, Englewood Cliffs, N.J., 1972, pp. 149-248.

Google Scholar

Cited By

View all

Pilipczuk MWrochna M(2018)On Space Efficiency of Algorithms Working on Structural Decompositions of GraphsACM Transactions on Computation Theory10.1145/31548569:4(1-36)Online publication date: 12-Jan-2018
https://dl.acm.org/doi/10.1145/3154856
Pallavoor RRaskhodnikova SVarma N(2017)Parameterized Property Testing of FunctionsACM Transactions on Computation Theory10.1145/31552969:4(1-19)Online publication date: 14-Dec-2017
https://dl.acm.org/doi/10.1145/3155296
Iwama KYoshida Y(2017)Parameterized TestabilityACM Transactions on Computation Theory10.1145/31552949:4(1-16)Online publication date: 14-Dec-2017
https://dl.acm.org/doi/10.1145/3155294
Show More Cited By

Recommendations

The denotational semantics of programming languages

This paper is a tutorial introduction to the theory of programming language semantics developed by D. Scott and C. Strachey. The application of the theory to formal language specification is demonstrated and other applications are surveyed. The first ...
Formalized structured analysis specifications
A denotational semantics implementation system

Reviews

Reviewer: John D. McLean

Denotational semantics has well-documented advantages over operational semantics and axiomatic semantics [1]. This paper helps overcome a traditional disadvantage of denotational semantics, that it provides little help for writing a language processor. A denotational semantics for a programming language maps syntactic constructs onto mathematical entities, which in turn can be defined using semantic algebras. These algebras can then be treated as rewrite rules and used to generate a language processor if the store argument can be treated as a single global variable. Schmidt gives sufficient criteria for this to be the case. The paper is clearly written and of value in making denotational semantics more practical. Yet, I wonder if time might be better spent pursuing other semantic approaches that more easily support processor development, using denotational semantics as a foundational underpinning.

Access critical reviews of Computing literature here

Become a reviewer for Computing Reviews.

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Programming Languages and Systems

ACM Transactions on Programming Languages and Systems Volume 7, Issue 2

Lecture notes in computer science Vol. 174

April 1985

175 pages

ISSN:0164-0925

EISSN:1558-4593

DOI:10.1145/3318

Editor:
Susan L. Graham
Univ. of California at Berkeley, Berkeley

Issue’s Table of Contents

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 April 1985

Published in TOPLAS Volume 7, Issue 2

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

117
Total Citations
View Citations
476
Total Downloads

Downloads (Last 12 months)59
Downloads (Last 6 weeks)11

Reflects downloads up to 03 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Pilipczuk MWrochna M(2018)On Space Efficiency of Algorithms Working on Structural Decompositions of GraphsACM Transactions on Computation Theory10.1145/31548569:4(1-36)Online publication date: 12-Jan-2018
Pallavoor RRaskhodnikova SVarma N(2017)Parameterized Property Testing of FunctionsACM Transactions on Computation Theory10.1145/31552969:4(1-19)Online publication date: 14-Dec-2017
Iwama KYoshida Y(2017)Parameterized TestabilityACM Transactions on Computation Theory10.1145/31552949:4(1-16)Online publication date: 14-Dec-2017
Chang C(2017)Metric 1-Median SelectionACM Transactions on Computation Theory10.1145/31548589:4(1-23)Online publication date: 14-Dec-2017
Chakraborty DTewari R(2017)An O(nϵ) Space and Polynomial Time Algorithm for Reachability in Directed Layered Planar GraphsACM Transactions on Computation Theory10.1145/31548579:4(1-11)Online publication date: 5-Dec-2017
Cherupalli HDuwe HYe WKumar RSartori J(2017)Determining Application-specific Peak Power and Energy Requirements for Ultra-low Power ProcessorsACM SIGPLAN Notices10.1145/3093336.303771152:4(3-16)Online publication date: 4-Apr-2017
Drey ZTeodorov CStorm TBalland EVarro D(2016)Object-oriented design pattern for DSL program monitoringProceedings of the 2016 ACM SIGPLAN International Conference on Software Language Engineering10.1145/2997364.2997373(70-83)Online publication date: 20-Oct-2016
Storm TBalland EVarro D(2016)Proceedings of the 2016 ACM SIGPLAN International Conference on Software Language EngineeringundefinedOnline publication date: 20-Oct-2016
Rosendahl M(2013)Abstract Interpretation as a Programming LanguageElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.129.7129(84-104)Online publication date: 19-Sep-2013
Zhang ZLi XChen Y(2012)Deciphering word-of-mouth in social mediaACM Transactions on Management Information Systems10.1145/2151163.21511683:1(1-23)Online publication date: 10-Apr-2012
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Cited By

Index Terms

Recommendations

The denotational semantics of programming languages

Formalized structured analysis specifications

A denotational semantics implementation system

Reviews

Access critical reviews of Computing literature here