Denotational Abstract Interpretation of Logic Programs

Kim Marriott, Harald Søndergaard, Neil D. Jones

Research output: Contribution to journalArticleResearchpeer-review

56 Citations (Scopus)

Abstract

Logic-programming languages are based on a principle of separation “logic” and “control.”. This means that they can be given simple model-theoretic semantics without regard to any particular execution mechanism 1994. Although the separation is desirable from a semantical point of view, it makes sound, efficient implementation of logic-programming languages difficult. The lack of “control information” in programs calls for complex data-flow analysis techniques to guide execution. Since data-flow analysis furthermore finds extensive use in error-finding and transformation tools, there is a need for a simple and powerful theory of data-flow analysis of logic programs. This paper offers such a theory, based on F. Nielson's extension of P. Cousot and R. Cousot's abstract interpretation. We present a denotational definition of the semantics of definite logic programs. This definition is of interest in its own right because of its compactness. Stepwise we develop the definition into a generic data-flow analysis that encompasses a large class of data-flow analyses based on the SLD execution model. We exemplify one instance of the definition by developing a provably correct groundness analysis to predict how variables may be bound to ground terms during execution. We also discuss implementation issues and related work.

Original languageEnglish
Pages (from-to)607-648
Number of pages42
JournalACM Transactions on Programming Languages and Systems
Volume16
Issue number3
DOIs
Publication statusPublished - 5 Jan 1994

Keywords

  • abstract interpretation
  • Boolean functions
  • dataflow analysis
  • global analysis
  • groundness analysis

Cite this