Notes for a Tutorial on Abstract Interpretation of Logic Programs

Abstract

The present notes are concerned with semantics-based dataflow analysis of definite clause logic programs. They have been produced for a tutorial given by the authors to the North American Conference on Logic Programming in Cleveland, Ohio, 16 October 1989. Thenotes are a condensed version of two forthcoming papers [33, 36]. Proofs omitted here appear in these papers. In Section 1 we give a brief introduction and historical background to the subject. In Section 2 we introduce some preliminary notation. In Section 3 we give a general theory for dataflow analysis which is basically that of abstract interpretation as introduced by P. and R. Cousot. We develop a simple abstract interpretation based on the well-known TP semantics of definite clause programs. In Section 4 we consider the abstract interpretation of definite clause logic programs and detail its uses. We discuss the limitations of dataflow analyses which are based on either the TP or SLD semantics of logic programs and develop a denotational semantics which may be used as a basis for most existing dataflow analyses. In Section 5 a non-trivial dataflow analysis for groundness propagation is developed from the denotational definitions given in Section 4. 1