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..