Advertisement

Strong abstract interpretation using power domains

Extended abstract
  • A. Mycroft
  • F. Nielson
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 154)

Abstract

Using a suitable notion of powerdomain we extend Abstract Interpretation to deal with partial functions so that non-termination is regarded as a specific value. We use this to validate a data flow analysis aimed at justifying when call-by-name can be implemented as call-by-value.

Keywords

Partial Order Abstract Interpretation Program Transformation Standard Semantic Induction Principle 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [1]
    K. Apt, G. Plotkin: A Cook's Tour of Countable Nondeterminism, Proceedings ICALP 1981, Lecture Notes in Computer Science 115, pp. 479–494, (Springer-Verlag, Berlin, 1981).Google Scholar
  2. [2]
    P. Cousot, R. Cousot: Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints, Conf. Record of the 4th ACM Symposium on Principles of Programming Languages, 1977.Google Scholar
  3. [3]
    P. Cousot, R. Cousot: Static Determination of Dynamic Properties of Recursive Procedures, in: E.J. Neuhold, Ed., Formal Descriptions of Programming Concepts, pp. 237–277, (North-Holland, Amsterdam, 1978).Google Scholar
  4. [4]
    P. Cousot, R. Cousot: Systematic Design of Program Analysis Frameworks, Conf. Record of the 6th ACM Symposium on Principles of Programming Languages, 1979.Google Scholar
  5. [5]
    V. Donzeau-Gouge: Utilisation de la Sémantique Dénotationelle Pour l'étude d'Interprétations Non-Standard, Rapport de Recherche, No. 273, INRIA, Rocquencourt, Le Chesnay, France, 1978.Google Scholar
  6. [6]
    M. Hennessy, G. Plotkin: Full Abstraction for a Simple Parallel Programming Language, Proceedings MFCS 1979, Lecture Notes in Computer Science 74, pp. 108–120, (Springer-Verlag, 1979).Google Scholar
  7. [7]
    M. Hennessy: Powerdomains and Nondeterministic Recursive Definitions, 5th Int. Symp. on Programming, Lecture Notes in Computer Science 137, (Springer-Verlag, 1982).Google Scholar
  8. [8]
    N. Jones: Flow Analysis of Lambda Expressions, Proceedings ICALP 1981, Lecture Notes in Computer Science 115, pp. 114–128, (Springer-Verlag, Berlin, 1981).Google Scholar
  9. [9]
    N. Jones, S. Muchnick: Complexity of Flow Analysis, Inductive Assertion Synthesis and a Language Due to Dijkstra, in S. Muchnick and N. Jones, Eds., Program Flow Analysis: Theory and Applications, pp. 380–393, (Prentice-Hall, New Jersey, 1981).Google Scholar
  10. [10]
    G. Kildall: A Unified Approach to Global Program Optimization, Conf. Record of ACM Symposium on Principles of Programming Languages, 1973.Google Scholar
  11. [11]
    J. Kam, J. Ullman: Monotonic Data Flow Analysis Frameworks, Acta Informatica 7, 1977.Google Scholar
  12. [12]
    R. Milne, C. Strachey: A Theory of Programming Language Semantics, Chapman and Hall, London, 1976.Google Scholar
  13. [13]
    A. Mycroft: The Theory and Practice of Transforming Call-by-need into Call-by-value. Proc. 4th Int. Symp. on Programming, Lecture Notes in Computer Science 83, (Springer-Verlag, 1980).Google Scholar
  14. [14]
    A. Mycroft: Abstract Interpretation and Optimising Transformations for Applicative Programs, Ph.D. thesis, University of Edinburgh, 1981.Google Scholar
  15. [15]
    F. Nielson: A Denotational Framework for Data Flow Analysis, Acta Informatica 18, 265–287 (1982).Google Scholar
  16. [16]
    F. Nielson: Towards Viewing Nondeterminism as Abstract Interpretation, University of Edinburgh, 1983.Google Scholar
  17. [17]
    G. Plotkin: A Powerdomain Construction, Siam J. Comput. 5,3 (1976), pp.452–487.Google Scholar
  18. [18]
    G. Plotkin: A Powerdomain for Countable Nondeterminism, Proceedings ICALP 1982, Lecture Notes in Computer Science 140, pp. 418–428, (Springer-Verlag, Berlin, 1982).Google Scholar
  19. [19]
    B. Rosen: Monoids for Rapid Data Flow Analysis, Siam J. Comput. 9, 1 (1980).Google Scholar
  20. [20]
    M. Sharir: Data Flow Analysis of Applicative Programs, Proceedings ICALP 1981, Lecture Notes in Computer Science 115, pp. 98–113, (Springer-Verlag, Berlin, 1981).Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1983

Authors and Affiliations

  • A. Mycroft
    • 1
  • F. Nielson
    • 1
  1. 1.Dept. of Computer ScienceUniversity of EdinburghScotland

Personalised recommendations