Skip to main content
SpringerLink
Log in

Optimal data flow analysis via observational equivalence

  • Communications
  • Conference paper
  • First Online:
Mathematical Foundations of Computer Science 1989 (MFCS 1989)

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

Abstract

In [18] a three level model was presented to establish a concept of completeness or optimality for data flow analysis algorithms in the framework of abstract interpretation [2]. The notion of observational equivalence introduced here generalizes the idea of the three level model, which can only deal with hierarchies of abstract interpretations. Investigating this more general notion, it actually turns out that the three level model is general in a theoretical sense: it determines the most abstract computation level which delivers complete results. However, consideration of other aspects of data flow analysis profit from the extra generality of our observation directed approach. For example the completeness or optimality proof for a “real life” optimizer could be shortened significantly this way.

The author is supported by the Science and Engineering Research Council grant GC/D69464

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. G. L. Burn, C. L. Hankin, and S. Abramsky. The theory of strictness analysis for higher order functions. Science of Computer Programming, 7:249–278, 1986.

    Google Scholar 

  2. P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In 4th POPL, pages 238–252, 1977.

    Google Scholar 

  3. P. Cousot and R. Cousot. Automatic synthesis of optimal invariant assertions: Mathematical foundations. ACM Sigplan Notices, 12:1–12, 1977.

    Google Scholar 

  4. P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In 6th POPL, pages 269–282, 1979.

    Google Scholar 

  5. R. De Nicola and M. Hennessy. Testing equivalences for processes. Theoretical Computer Science, 34:83–133, 1984.

    Google Scholar 

  6. C. A. R. Hoare and H. Jifeng. Data refinement in a categorical setting. Technical report, Oxford University, Computing Laboratory, Programming Research Group, February 1988.

    Google Scholar 

  7. J. B. Kam and J. D. Ullman. Monotone data flow analysis frameworks. Acta Informatica, 7:309–317, 1975.

    Google Scholar 

  8. R. Milner. Fully abstract models of typed lambda calculi. Theoretical Computer Science, 4:1–22, 1977.

    Google Scholar 

  9. A. Mycroft. Abstract Interpretation and Optimizing Transformations for Applicative Programs. PhD thesis, Edinburgh Univ., Dept. of Comp. Sci., 1981.

    Google Scholar 

  10. A. Mycroft and F. Nielson. Strong abstract interpretation using power domains. In ICALP '83, pages 536–547. LNCS 154, 1983.

    Google Scholar 

  11. F. Nielson. Abstract interpretation of denotational definitions. In STACS '86, pages 1–20. LNCS 210, 1986.

    Google Scholar 

  12. F. Nielson. A bibliography on abstract interpretations. ACM Sigplan Notices, 21:31–38, 1986.

    Google Scholar 

  13. F. Nielson. Strictness analysis and denotational abstract interpretation. In 14th POPL, pages 120–131, Munich, West-Germany, 1987.

    Google Scholar 

  14. H. R. Nielson and F. Nielson. Pragmatic aspects of two-level denotational meta-languages. In ESOP '86, pages 133–143. LNCS 213, 1986.

    Google Scholar 

  15. B. K. Rosen, M. N. Wegmann, and F. K. Zadeck. Global value numbers and redundant computations. In 15th POPL, pages 12–27, San Diego, California, 1988.

    Google Scholar 

  16. D. Sannella and A. Tarlecki. On observational equivalence and algebraic specifications. Journal of Computer and System Sciences, pages 150–178, 1987.

    Google Scholar 

  17. B. Steffen. Abstrakte Interpretationen beim Optimieren von Programmlaufzeiten. Ein Optimalitätskonzept und seine Anwendung. PhD thesis, Christian-Albrechts-Universität Kiel, 1987.

    Google Scholar 

  18. B. Steffen. Optimal run time optimization — proved by a new look at abstract interpretations. In TAPSOFT '87, pages 52–68. LNCS 249, 1987.

    Google Scholar 

  19. B. Steffen and M. Mendler. Compositional characterization of observable program properties. LFCS report series, LFCS, Edinburgh Univ., Dept. of Comp. Sci., 1989.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Laboratory for Foundations of Computer Science, University of Edinburgh, UK

    Bernhard Steffen

Authors
  1. Bernhard Steffen
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Antoni Kreczmar Grazyna Mirkowska

Rights and permissions

Reprints and permissions

Copyright information

© 1989 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Steffen, B. (1989). Optimal data flow analysis via observational equivalence. In: Kreczmar, A., Mirkowska, G. (eds) Mathematical Foundations of Computer Science 1989. MFCS 1989. Lecture Notes in Computer Science, vol 379. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-51486-4_95

Download citation

  • DOI: https://doi.org/10.1007/3-540-51486-4_95

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-51486-2

  • Online ISBN: 978-3-540-48176-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation