Bottom-up dataflow analysis of normal logic programs

Kim Marriott, Harald Søndergaard

Research output: Contribution to journalArticleResearchpeer-review

27 Citations (Scopus)

Abstract

A theory of semantics-based dataflow analysis using a notion of "insertion" is presented. This notion relaxes the Galois connections used in Cousot and Cousot's theory of abstract interpretation. The aim is to obtain a firm basis for the development of dataflow analyses of normal logic programs. A dataflow analysis is viewed as a nonstandard semantics that approximates the standard semantics by manipulating descriptions of data objects rather than the objects themselves. A Kleene logic-based semantics for normal logic programs is defined, similar to Fitting's f{cyrillic}P semantics. This provides the needed semantic base for "bottom-up" dataflow analyses. Such analyses give information about the success and failure sets of a program. A major application of bottom-up analysis is therefore type inference. We detail a dataflow analysis using descriptions similar to Sato and Tamaki's depth-k abstractions and another using Marriott, Naish, and Lassez's "singleton" abstractions. We show that both are sound with respect to our semantics and outline various uses of the analyses. Finally we justify our choice of semantics by showing that it is the most abstract of a number of possible semantics. This means that every analysis based on our semantics is correct with respect to these other semantics, including Kunen's semantics, SLDNF resolution, and the common (sound) PROLOG semantics.

Original languageEnglish
Pages (from-to)181-204
Number of pages24
JournalThe Journal of Logic Programming
Volume13
Issue number2-3
DOIs
Publication statusPublished - 1 Jan 1992

Cite this

Marriott, Kim ; Søndergaard, Harald. / Bottom-up dataflow analysis of normal logic programs. In: The Journal of Logic Programming. 1992 ; Vol. 13, No. 2-3. pp. 181-204.
@article{12f5c66face94835bb705d7ac5a39a32,
title = "Bottom-up dataflow analysis of normal logic programs",
abstract = "A theory of semantics-based dataflow analysis using a notion of {"}insertion{"} is presented. This notion relaxes the Galois connections used in Cousot and Cousot's theory of abstract interpretation. The aim is to obtain a firm basis for the development of dataflow analyses of normal logic programs. A dataflow analysis is viewed as a nonstandard semantics that approximates the standard semantics by manipulating descriptions of data objects rather than the objects themselves. A Kleene logic-based semantics for normal logic programs is defined, similar to Fitting's f{cyrillic}P semantics. This provides the needed semantic base for {"}bottom-up{"} dataflow analyses. Such analyses give information about the success and failure sets of a program. A major application of bottom-up analysis is therefore type inference. We detail a dataflow analysis using descriptions similar to Sato and Tamaki's depth-k abstractions and another using Marriott, Naish, and Lassez's {"}singleton{"} abstractions. We show that both are sound with respect to our semantics and outline various uses of the analyses. Finally we justify our choice of semantics by showing that it is the most abstract of a number of possible semantics. This means that every analysis based on our semantics is correct with respect to these other semantics, including Kunen's semantics, SLDNF resolution, and the common (sound) PROLOG semantics.",
author = "Kim Marriott and Harald S{\o}ndergaard",
year = "1992",
month = "1",
day = "1",
doi = "10.1016/0743-1066(92)90031-W",
language = "English",
volume = "13",
pages = "181--204",
journal = "Journal of Logic Programming",
issn = "0743-1066",
number = "2-3",

}

Bottom-up dataflow analysis of normal logic programs. / Marriott, Kim; Søndergaard, Harald.

In: The Journal of Logic Programming, Vol. 13, No. 2-3, 01.01.1992, p. 181-204.

Research output: Contribution to journalArticleResearchpeer-review

TY - JOUR

T1 - Bottom-up dataflow analysis of normal logic programs

AU - Marriott, Kim

AU - Søndergaard, Harald

PY - 1992/1/1

Y1 - 1992/1/1

N2 - A theory of semantics-based dataflow analysis using a notion of "insertion" is presented. This notion relaxes the Galois connections used in Cousot and Cousot's theory of abstract interpretation. The aim is to obtain a firm basis for the development of dataflow analyses of normal logic programs. A dataflow analysis is viewed as a nonstandard semantics that approximates the standard semantics by manipulating descriptions of data objects rather than the objects themselves. A Kleene logic-based semantics for normal logic programs is defined, similar to Fitting's f{cyrillic}P semantics. This provides the needed semantic base for "bottom-up" dataflow analyses. Such analyses give information about the success and failure sets of a program. A major application of bottom-up analysis is therefore type inference. We detail a dataflow analysis using descriptions similar to Sato and Tamaki's depth-k abstractions and another using Marriott, Naish, and Lassez's "singleton" abstractions. We show that both are sound with respect to our semantics and outline various uses of the analyses. Finally we justify our choice of semantics by showing that it is the most abstract of a number of possible semantics. This means that every analysis based on our semantics is correct with respect to these other semantics, including Kunen's semantics, SLDNF resolution, and the common (sound) PROLOG semantics.

AB - A theory of semantics-based dataflow analysis using a notion of "insertion" is presented. This notion relaxes the Galois connections used in Cousot and Cousot's theory of abstract interpretation. The aim is to obtain a firm basis for the development of dataflow analyses of normal logic programs. A dataflow analysis is viewed as a nonstandard semantics that approximates the standard semantics by manipulating descriptions of data objects rather than the objects themselves. A Kleene logic-based semantics for normal logic programs is defined, similar to Fitting's f{cyrillic}P semantics. This provides the needed semantic base for "bottom-up" dataflow analyses. Such analyses give information about the success and failure sets of a program. A major application of bottom-up analysis is therefore type inference. We detail a dataflow analysis using descriptions similar to Sato and Tamaki's depth-k abstractions and another using Marriott, Naish, and Lassez's "singleton" abstractions. We show that both are sound with respect to our semantics and outline various uses of the analyses. Finally we justify our choice of semantics by showing that it is the most abstract of a number of possible semantics. This means that every analysis based on our semantics is correct with respect to these other semantics, including Kunen's semantics, SLDNF resolution, and the common (sound) PROLOG semantics.

UR - http://www.scopus.com/inward/record.url?scp=38249013209&partnerID=8YFLogxK

U2 - 10.1016/0743-1066(92)90031-W

DO - 10.1016/0743-1066(92)90031-W

M3 - Article

VL - 13

SP - 181

EP - 204

JO - Journal of Logic Programming

JF - Journal of Logic Programming

SN - 0743-1066

IS - 2-3

ER -