Abstract interpretation of denotational definitions

A survey
  • Flemming Nielson
Contributed Papers
Part of the Lecture Notes in Computer Science book series (LNCS, volume 210)


Abstract interpretation is a framework for describing data flow analyses and for proving their correctness. Traditionally the framework is developed for flow chart languages, but this paper extends the applicability of the idea to a wide class of languages that have a denotational semantics. The main idea is to study a denotational metalanguage with two kinds of types: one kind describes compile-time entities and another describes run-time entities. The run-time entities will be interpreted differently so as to obtain different semantics from the same denotational definition: the standard semantics is the ordinary semantics, an approximating semantics describes a data flow analysis and the collecting semantics is a convenient tool in relating the previous two semantics.


Abstract Interpretation Covariant Functor Denotational Semantic Standard Semantic Structural Induction 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [AhUl 78]
    A.V. Aho, J.D. Ullman: Principles of Compiler Design, Addison-Wesley, 1978.Google Scholar
  2. [ArMa 75]
    M.A. Arbib, E.G. Manes: Arrows, Structures and Functors: The Categorical Imperative, Academic Press, 1975.Google Scholar
  3. [BuHA 85]
    G.L. Burn, C.L. Hankin, S. Abramsky: The Theory and Practice of Strictness Analysis for Higher Order Functions, Research Report DoC 85/6, Imperial College of Science and Technology, London.Google Scholar
  4. [CoCo 77]
    P. Cousot, R. Cousot: Abstract Interpretation: A Unified lattice model for static analysis of programs by construction or approximation of fixpoints, in: Conf. Record of the 4th ACM Symposium on Principles of Programming Languages, 1977.Google Scholar
  5. [CoCo 78]
    P. Cousot, R. Cousot: Static determination of dynamic properties of recursive procedures, in: Formal Descriptions of Programming Concepts, E.J. Neuhold (ed.), North-Holland Publishing Company, 1978.Google Scholar
  6. [CoCo 79]
    P. Cousot, R. Cousot: Systematic design of program analysis frameworks, in: Conf. Record of the 6th ACM Symposium on Principles of Programming Languages, 1979.Google Scholar
  7. [Don 78]
    V. Donzeau-Gouge: Utilisation de la sémantique dénotationelle pour l'étude d'interprétations non-standard, IRIA report No. 273, France, 1978.Google Scholar
  8. [Don 81]
    V. Donzeau-Gouge: Denotational definition of properties of program computations, in: Program Flow Analysis: Theory and Applications, S.S. Muchnick, N.D. Jones (eds.), Prentice-Hall, 1981.Google Scholar
  9. [Gor 79]
    M. Gordon: The Denotational Description of Programming Languages — An Introduction, Springer-Verlag, 1979.Google Scholar
  10. [Hec 77]
    M.S. Hecht: Flow Analysis of Computer Programs, North-Holland, 1977.Google Scholar
  11. [JoMu 78]
    N.D. Jones, S.S. Muchnick: TEMPO: A Unified Treatment of Binding Time and Parameter Passing Concepts in Programming Languages, Lecture Notes in Computer Science No. 66, Springer Verlag, 1978.Google Scholar
  12. [JoMu 81]
    N.D. Jones, S.S. Muchnick: Complexity of flow analysis, inductive assertion synthesis and a language due to Dijkstra, in: Program Flow Analysis: Theory and Applications, S.S. Muchnick, N.D. Jones (eds.), Prentice-Hall, 1981.Google Scholar
  13. [KaUl 77]
    J.B. Kam, J.D. Ullman: Monotone data flow analysis frameworks, Acta Informatica, vol. 7 (1977), pp. 305–317.CrossRefGoogle Scholar
  14. [MiSt 76]
    R. Milne, C. Strachey: A Theory of Programming Language Semantics, Chapman and Hall, London, 1976.Google Scholar
  15. [MyNi 83]
    A. Mycroft, F. Nielson: Strong abstract interpretation using power domains, in: Proceedings ICALP 1983, Springer LNCS no. 154, pp. 536–547.Google Scholar
  16. [Nie 82]
    F. Nielson: A denotational framework for data flow analysis, Acta Informatica, vol. 18 (1982), pp. 265–287.CrossRefGoogle Scholar
  17. [Nie 84]
    F. Nielson: Abstract Interpretation Using Domain Theory, Ph.D. thesis, University of Edinburgh, Scotland, 1984.Google Scholar
  18. [Nie 85a]
    F. Nielson: Tensor Products Generalize the Relational Data Flow Analysis Method, 4'th HCSC, 1985.Google Scholar
  19. [Nie 85b]
    F. Nielson: Expected Forms of Data Flow Analysis, to appear in: Proceedings of "Programs as Data Objects", Springer LNCS, 1986.Google Scholar
  20. [NiNi 85a]
    F. Nielson, H.R. Nielson: Code Generation from Two-Level Denotational Meta-Languages, to appear in: Proceedings of "Programs as Data Objects", Springer LNCS, 1986.Google Scholar
  21. [NiNi 85b]
    H.R. Nielson, F. Nielson: Pragmatic Aspects of Two-Level Denotational Meta-Languages, report R-85-13, Aalborg University Centre, Denmark.Google Scholar
  22. [Rey 74]
    J.C. Reynolds: On the Relation between Direct and Continuation Semantics, in: Proceedings 2nd ICALP 1974, Lecture Notes in Computer Science 14, pp. 141–156.Google Scholar
  23. [Ros 77]
    B.K. Rosen: High-level data flow analysis, CACM vol. 20 No. 10 (1977), pp. 712–724.Google Scholar
  24. [SmP1 82]
    M.B. Smyth, G.D. Plotkin: The category-theoretic solution of recursive domain equations, SIAM J. Comput., vol. 11 No. 4 (1982), pp. 761–783.Google Scholar
  25. [Ten 74]
    A. Tenenbaum: Automatic Type Analysis in a Very High Level Language, Ph.D. thesis, New York University, 1974.Google Scholar
  26. [Ten 81]
    R.D. Tennent: Principles of Programming Languages, Prentice-Hall, 1981.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1985

Authors and Affiliations

  • Flemming Nielson
    • 1
  1. 1.Institute of Electronic SystemsAalborg University CentreAalborg C.Denmark

Personalised recommendations