Skip to main content
SpringerLink
Log in

Natural-semantics-based abstract interpretation (preliminary version)

  • Invited Talks
  • Conference paper
  • First Online:
Static Analysis (SAS 1995)

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

Included in the following conference series:

Abstract

The original formulation of abstract interpretation (a.i.) [5] demonstrated clearly that a.i. is a formal-semantics-based methodology for deriving a provably correct, convergent, canonical iterative data flow analysis from a standard semantics of a programming language. But subsequent research in a.i. has obscured the methodology of the topic. For example, the recent slew of papers on closures analysis [2, 3, 17, 18, 21, 37, 39, 40, 41, 42, 43] mix implementation optimizations with specifications and leave unclear exactly what closures analysis is. In this paper, we reexamine the principles of a.i. and reformulate the topic on a foundation of coinductively defined natural semantics. We aim to demonstrate that the intensional and compositional aspects of natural semantics make it an ideal vehicle for formulating abstract interpretations of problems while preserving the essential characteristics of the subject.

Partially supported by NSF CCR-9302962 and ONR N00014-94-1-0866.

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. A. Aho, R. Sethi, and J. Ullman. Compilers: Principles, Techniques, and Tools. Addison Wesley, 1986.

    Google Scholar 

  2. A. Banerjee. The Semantics and Implementation of Bindings in Higher-Order Programming Languages. PhD thesis, Kansas State University, 1995.

    Google Scholar 

  3. A. Bondorf. Automatic autoprojection of higher order recursive equations. Science of Computer Programming, 17:3–34, 1991.

    Google Scholar 

  4. G. L. Burn, C. Hankin, and S. Abramsky. Strictness analysis for higher-order functions. Science of Computer Programming, 7:249–278, 1986.

    Google Scholar 

  5. P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs. In Proc. 4th ACM Symp. on Principles of Programming Languages, pages 238–252. ACM Press, 1977.

    Google Scholar 

  6. P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In Proc. 6th ACM Symp. on Principles of Programming Languages, pages 269–282. ACM Press, 1979.

    Google Scholar 

  7. P. Cousot and R. Cousot. Inductive definitions, semantics, and abstract interpretation. In Proc. 19th ACM Symp. on Principles of Programming Languages, pages 83–94. ACM Press, 1992.

    Google Scholar 

  8. P. Cousot and R. Cousot. Higher-order abstract interpretation. In Proc. IEEE Int'l. Conf. Programming Languages. IEEE Press, 1994.

    Google Scholar 

  9. Th. Despeyroux. Executable specification of static semantics. In G. Kahn, D.B. MacQueen, and G. Plotkin, editors, Semantics of Data Types, pages 215–234. Lecture Notes in Computer Science 173, Springer-Verlag, 1984.

    Google Scholar 

  10. V. Donzeau-Gouge. Denotational definition of properties of program's computations. In S. Muchnick and N.D. Jones, editors, Program Flow Analysis: Theory and Applications. Prentice-Hall, 1981.

    Google Scholar 

  11. J. Goguen, J. Thatcher, E. Wagner, and J. Wright. Initial algebra semantics and continuous algebras. J. ACM, 24:68–95, 1977.

    Google Scholar 

  12. V. Gouranton and D. LeMétayer. Derivation of static analysers of functional programs from path properties of a natural semantics. Technical Report Research Report 2607, INRIA, 1995.

    Google Scholar 

  13. I. Guessarian. Algebraic Semantics. Springer Lecture Notes in Computer Science 99. Springer-Verlag, 1981.

    Google Scholar 

  14. C. Gunter. Foundations of Programming Languages. MIT Press, Cambridge, MA, 1992.

    Google Scholar 

  15. M. Hecht. Flow Analysis of Computer Programs. Elsevier, 1977.

    Google Scholar 

  16. P. Hudak and J. Young. A collecting interpretation of expressions (without powerdomains). In Proc. 15th ACM Symp. on Principles of Programming Languages, pages 107–118. ACM Press, 1988.

    Google Scholar 

  17. S. Jagannathan and S. Weeks. A unified treatment of flow analysis in higher-order languages. In Proc. 22d. ACM Symp. Principles of Programming Languages, pages 393–407, 1995.

    Google Scholar 

  18. S. Jagannathan and A. Wright. Effective flow analysis for avoiding run-time checks. In Proc. Workshop on types for program analysis, number http://www.daimi.aau.dk/∼bra8130/TPA/proceedings.html, Univ. of Aarhus, Denmark, 1995.

    Google Scholar 

  19. N.D. Jones and S. Muchnick. Flow analysis and optimization of LISP-like structures. In Proc. 6th. ACM Symp. Principles of Programming Languages, pages 244–256, 1979.

    Google Scholar 

  20. N.D. Jones and A. Mycroft. Data flow analysis of applicative programs using minimal function graphs. In Proc. 13th Symp. on Principles of Prog. Languages, pages 296–306. ACM Press, 1986.

    Google Scholar 

  21. N.D. Jones and M. Rosendahl. Higher-order minimal function graphs. In ??? ???, 1994.

    Google Scholar 

  22. G. Kahn. Natural semantics. In Proc. STACS '87, pages 22–39. Lecture Notes in Computer Science 247, Springer, Berlin, 1987.

    Google Scholar 

  23. J. Kam and J. Ullman. Global data flow analysis and iterative algorithms. J. ACM, 23:158–171, 1976.

    Google Scholar 

  24. G. Kildall. A unified approach to global program optimization. In Proc. ACM Symp. on Principles of Programming Languages, 1973.

    Google Scholar 

  25. P. Lewis, D. Rosenkrantz, and R. Stearns. Compiler Design Theory. Addison-Wesley, 1978.

    Google Scholar 

  26. A. Melton, G. Strecker, and D. Schmidt. Galois connections and computer science applications. In Category Theory and Computer Programming, pages 299–312. Lecture Notes in Computer Science 240, Springer-Verlag, 1985.

    Google Scholar 

  27. R. Milner and M. Tofte. Co-induction in relational semantics. Theoretical Computer Science, 17:209–220, 1992.

    Google Scholar 

  28. J. C. Mitchell. Type systems for programming languages. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, chapter 8, pages 367–458. Elsevier Science Publishers, 1990.

    Google Scholar 

  29. M. Mizuno and D. Schmidt. A security flow control algorithm and its denotational semantics correctness proof. Formal Aspects of Computing, 4:727–754, 1992.

    Google Scholar 

  30. S. Muchnick and N.D. Jones, editors. Program Flow Analysis: Theory and Applications. Prentice-Hall, 1981.

    Google Scholar 

  31. A. Mycroft. Abstract interpretation and optimizing transformations for recursive programs. PhD thesis, Edinburgh University, 1981.

    Google Scholar 

  32. A. Mycroft and N.D. Jones. A relational framework for abstract interpretation. In Programs as Data Objects, pages 156–171. Lecture Notes in Computer Science 217, Springer-Verlag, 1985.

    Google Scholar 

  33. F. Nielson. Semantic foundations of data flow analysis. Technical Report Report DAIMI PB-131, Aarhus University, Denmark, 1981.

    Google Scholar 

  34. F. Nielson. A denotational framework for data flow analysis. Acta Informatica, 18:265–287, 1982.

    Google Scholar 

  35. F. Nielson. Program transformations in a denotational setting. ACM Trans. Prog. Languages and Systems, 7:359–379, 1985.

    Google Scholar 

  36. F. Nielson. Two-level semantics and abstract interpretation. Theoretical Computer Science, 69(2):117–242, 1989.

    Google Scholar 

  37. J. Palsberg. Global program analysis in constraint form. In M. P. Fourman, P. T. Johnstone, and A. M. Pitts, editors, Proc. CAAP'94, Lecture Notes in Computer Science, pages 258–269. Springer-Verlag, 1994.

    Google Scholar 

  38. G. D. Plotkin. Lambda-definability in the full type hierarchy. In J. Seldin and J. Hindley, editors, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 363–374. Academic Press, 1980.

    Google Scholar 

  39. P. Sestoft. Replacing function parameters by global variables. In Proc. Functional Programming and Computer Architecture, pages 39–53. ACM Press, 1989.

    Google Scholar 

  40. P. Sestoft. Analysis and Efficient Implementation of Functional Programs. PhD thesis, Copenhagen University, 1991.

    Google Scholar 

  41. O. Shivers. Control-flow analysis in Scheme. In Proc. SIGPLAN88 Conf. on Prog. Language Design and Implementation, pages 164–174, 1988.

    Google Scholar 

  42. O. Shivers. Control Flow Analysis of Higher-Order Languages. PhD thesis, Carnegie Mellon University, 1991.

    Google Scholar 

  43. D. Stefanescu and Y. Zhou. An equational framework for flow analysis of higher-order functional programs. In Proc. 1994 ACM Conf. on Lisp and Functional Programming, pages 318–327. ACM Press, 1994.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computing and Information Sciences, Kansas State University, 66506, Manhattan, KS, USA

    David A. Schmidt

Authors
  1. David A. Schmidt
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Alan Mycroft

Rights and permissions

Reprints and permissions

Copyright information

© 1995 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Schmidt, D.A. (1995). Natural-semantics-based abstract interpretation (preliminary version). In: Mycroft, A. (eds) Static Analysis. SAS 1995. Lecture Notes in Computer Science, vol 983. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60360-3_28

Download citation

  • DOI: https://doi.org/10.1007/3-540-60360-3_28

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-60360-3

  • Online ISBN: 978-3-540-45050-4

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation