article

Open access

Program transformations in a denotational setting

Author:

Flemming NielsonAuthors Info & Claims

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

Pages 359 - 379

https://doi.org/10.1145/3916.3917

Published: 01 July 1985 Publication History

PDF eReader

Abstract

Program transformations are frequently performed by optimizing compilers, and the correctness of applying them usually depends on data flow information. For language-to-same-language transformations, it is shown how a denotational setting can be useful for validating such program transformations.

Strong equivalence is obtained for transformations that exploit information from a class of forward data flow analyses, whereas only weak equivalence is obtained for transformations that exploit information from a class of backward data flow analyses. To obtain strong equivalence, both the original and the transformed program must be data flow analysed, but consideration of a transformation-exploiting liveness of variables indicates that a more satisfactory approach may be possible.

References

[1]

AHO, A. V., ANO ULLMAN, J.D. Principles o{ Compiler Design. Addison-Wesley, London, 1977.

Digital Library

Google Scholar

[2]

COUSOT, P., ANO COUSOT, R. Systematic design of program analysis frameworks. In Proceedings 6th ACM Symposium on Principles of Programming Languages (1979), ACM, New York, 269- 282.

Digital Library

Google Scholar

[3]

COUSOT, P. Semantic foundations of program analysis. In Program Flow Analysis: Theory and Applications, S. S. Muchnick and N. D. Jones, Eds., Prentice-Hall, Englewood Cliffs, N.J., 1981, 303-342.

Google Scholar

[4]

GERHART, S. L. Correctness-preserving program transformations. In Proceedings 2nd ACM Symposium on Principles of Programming Languages (1975), ACM, New York, 54-66.

Digital Library

Google Scholar

[5]

HUET, G., ANO LANG, B. Proving and applying program transformations expressed with secondorder patterns. Acta In{. 11 (1978), 31-55.

Google Scholar

[6]

LOVEMAN, D.B. Program improvement by source-to-source transformations. J. ACM 24 (1977), 121-145.

Digital Library

Google Scholar

[7]

MILNE, R., AND STRACHEY, C. A Theory of Programming Language Semantics. Chapman and Hall, London, 1976.

Digital Library

Google Scholar

[8]

MILNER, R. Program semantics and mechanized proof. In Foundations of Computer Science II, K. R. Apt and J. W. de Bakker, Eds., Mathematical Centre Tracts 82, Amsterdam, 1976, 3-44.

Google Scholar

[9]

NIELSON, F. A denotational framework for data flow analysis. Acta Inf. 18 (1982), 265-287.

Digital Library

Google Scholar

[10]

ROSEN, B.K. Tree-manipulating systems and Church-Rosser theorems. J. ACM 20 (1973), 160-187.

Digital Library

Google Scholar

[11]

STOY, g.E. Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory. MIT Press, Cambridge, Mass., 1977.

Digital Library

Google Scholar

Cited By

View all

Xiong HDai QChang RQiu MWang RShen WZhou YChristakis MPradel M(2024)Atlas: Automating Cross-Language Fuzzing on Android Closed-Source LibrariesProceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis10.1145/3650212.3652133(350-362)Online publication date: 11-Sep-2024
https://dl.acm.org/doi/10.1145/3650212.3652133
Sharan P(2022)Automated Discrimination of Cough in Audio Recordings: A Scoping ReviewFrontiers in Signal Processing10.3389/frsip.2022.7596842Online publication date: 3-Jun-2022
https://doi.org/10.3389/frsip.2022.759684
Li XNielson FNielson H(2019)Enforcing globally dependent flow policies in message-passing systemsJournal of Computer Languages10.1016/j.cola.2019.10090454(100904)Online publication date: Oct-2019
https://doi.org/10.1016/j.cola.2019.100904
Show More Cited By

Index Terms

Program transformations in a denotational setting
1. Software and its engineering
  1. Software notations and tools
    1. Compilers
    2. Formal language definitions
      1. Semantics
2. Theory of computation
  1. Semantics and reasoning
    1. Program reasoning
      1. Program verification
    2. Program semantics
      1. Denotational semantics

Recommendations

Program transformations for verifying parameterized systems
Program transformations using temporal logic side conditions

This article describes an approach to program optimization based on transformations, where temporal logic is used to specify side conditions, and strategies are created which expand the repertoire of transformations and provide a suitable level of ...
Translating ATL Model Transformations to Algebraic Graph Transformations
Proceedings of the 8th International Conference on Theory and Practice of Model Transformations - Volume 9152

Analyzing and reasoning on model transformations has become very relevant for various applications such as ensuring the correctness of transformations. ATL is a model transformation language with rich semantics and a focus on usability, making its ...

Reviews

Reviewer: Jacek Gibert

Data flow analysis is a practical tool often used for transforming and optimizing programs during compilation. This theoretical paper proposes a formal mathematical framework that allows the validation of such program transformations. A toy language is defined to illustrate the abstract way of specifying both forward and backward data flow information by means of “collecting” and “future” semantics, respectively. Two results are achieved: (1) a strong equivalence between original and transformed programs for the collecting semantics; and (2) a weak equivalence between original and transformed programs for the future semantics. The paper attributes the weakness of the second result to an inherent insufficiency of present denotational approaches. For example, a strong equivalence can only be achieved for the future semantics if both the original and the transformed programs are data flow analyzed, contrary to what is done in practice. It remains to generalized denotational methods to overcome this problem. This paper is well presented and can easily be read by all those interested in the design of smart compilers or denotational semantics of programming languages. However, the first group may find that many semantical points, which have been addressed rigorously by this paper, are not worth taking up in a practical compiler design context, as efficiency issues have not been considered at all.

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 3

July 1985

134 pages

ISSN:0164-0925

EISSN:1558-4593

DOI:10.1145/3916

Editor:
Susan L. Graham

Issue’s Table of Contents

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 July 1985

Published in TOPLAS Volume 7, Issue 3

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

39
Total Citations
View Citations
377
Total Downloads

Downloads (Last 12 months)30
Downloads (Last 6 weeks)5

Reflects downloads up to 22 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Xiong HDai QChang RQiu MWang RShen WZhou YChristakis MPradel M(2024)Atlas: Automating Cross-Language Fuzzing on Android Closed-Source LibrariesProceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis10.1145/3650212.3652133(350-362)Online publication date: 11-Sep-2024
https://dl.acm.org/doi/10.1145/3650212.3652133
Sharan P(2022)Automated Discrimination of Cough in Audio Recordings: A Scoping ReviewFrontiers in Signal Processing10.3389/frsip.2022.7596842Online publication date: 3-Jun-2022
https://doi.org/10.3389/frsip.2022.759684
Li XNielson FNielson H(2019)Enforcing globally dependent flow policies in message-passing systemsJournal of Computer Languages10.1016/j.cola.2019.10090454(100904)Online publication date: Oct-2019
https://doi.org/10.1016/j.cola.2019.100904
Nielson HNielson FLi X(2015)Hoare Logic for Disjunctive Information FlowEssays Dedicated to Pierpaolo Degano on Programming Languages with Applications to Biology and Security - Volume 946510.5555/2963891.2963897(47-65)Online publication date: 1-Aug-2015
https://dl.acm.org/doi/10.5555/2963891.2963897
Nielson HNielson FLi X(2015)Hoare Logic for Disjunctive Information FlowProgramming Languages with Applications to Biology and Security10.1007/978-3-319-25527-9_6(47-65)Online publication date: 20-Nov-2015
https://doi.org/10.1007/978-3-319-25527-9_6
Schmidt D(2012)Inverse-limit and topological aspects of abstract interpretationTheoretical Computer Science10.1016/j.tcs.2012.01.002430(23-42)Online publication date: 1-Apr-2012
https://dl.acm.org/doi/10.1016/j.tcs.2012.01.002
Jouvelot PFeautrier P(2011)Parallélisation sémantiqueRAIRO - Theoretical Informatics and Applications10.1051/ita/199024020131124:2(131-159)Online publication date: 8-Jan-2011
https://doi.org/10.1051/ita/1990240201311
Chang MSmith EReitmaier RBebenita MGal AWimmer CEich BFranz MHosking ABacon DKrieger O(2009)Tracing for web 3.0Proceedings of the 2009 ACM SIGPLAN/SIGOPS international conference on Virtual execution environments10.1145/1508293.1508304(71-80)Online publication date: 11-Mar-2009
https://dl.acm.org/doi/10.1145/1508293.1508304
Schmidt D(2009)Abstract Interpretation From a Denotational-semantics PerspectiveElectronic Notes in Theoretical Computer Science (ENTCS)10.1016/j.entcs.2009.07.082249(19-37)Online publication date: 1-Aug-2009
https://dl.acm.org/doi/10.1016/j.entcs.2009.07.082
Burn GLe Métayer D(2008) Proving the correctness of compiler optimisations based on a global analysis: a study of strictness analysis † Journal of Functional Programming10.1017/S09567968000015816:1(75-109)Online publication date: 7-Nov-2008
https://doi.org/10.1017/S0956796800001581
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Get Access

Login options

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

Abstract

References

Cited By

Index Terms

Recommendations

Program transformations for verifying parameterized systems

Program transformations using temporal logic side conditions

Translating ATL Model Transformations to Algebraic Graph Transformations

Reviews

Access critical reviews of Computing literature here

Comments

Information

Published In

Publisher

Publication History

Permissions

Check for updates

Qualifiers

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

PDF

eReader

Get Access

Login options

Full Access

Figures

Other

Share

Share this Publication link

Share on social media

Affiliations