Practical Model-Based Static Analysis for Definite Logic ProgramsJ. P. Gallagher, D. Boulanger, H. Saglam, Practical Model-Based Static Analysis for Definite Logic Programs. Proceedings of the 1995 International Symposium on Logic Programming, December 1995, Portland, Oregon.. ISBN 0-262-62099-5, pp. 351–368. December 1995. No electronic version available.
The declarative semantics of definite programs is the basis of an elegant and practical framework for static analysis of definite logic programs. We define a core semantics parameterised by a pre-interpretation of the language underlying the program. The concrete semantics is given by an extended Herbrand interpretation, capturing the correct answers of a program. The semantics is computed as the least fixed point of an immediate consequences operator. An abstract semantics is specified simply by giving, for each constant and function in the program, a denotation in an abstract domain of interpretation. No abstract operations such as abstract unification need to be defined. The directness and simplicity of this approach is then illustrated by specifying and implementing a number of abstract interpretations. These include various mode analyses, analyses on the structure of lists and the length of lists, and simple and polymorphic types. The implementations used for the experiments are based on abstract compilation and existing bottom-up analysis tools. Even without any domain-specific optimisations, the results indicate that the approach is practical for many useful domains.