Bottom-up dataflow analysis of normal logic programs

AbstractA 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 ф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