Combining Logic and Control to Characterize Global Invariants of Prolog Programs.
Livio Colussi, Elena Marchiori, Massimo Marchiori · 1994
The behaviour of logic programs (with various built-in's) is described in terms of sets of substitutions associated with the control points of the program. These sets are defined by means of an operational semantics O, based on a description of unification as predicate transformer. It is shown that O subsumes the semantics of logic programs consisting of the set of computed substitutions obtained from finite prefixes of SLD-derivations with Prolog selection rule. Moreover O is used as base semantics for performing dataflow analysis of logic programs. 1 Introduction The standard view of logic programming is declarative, i.e., a program is a static description of some predicate or function, and there is no reference to the computational mechanism used to compute it. In the declarative interpretation, the meaning of a program is given model-theoretically as the set of all its logical consequences in the Herbrand domain of ground atoms ([vEK76]). Nevertheless, despite of its simplicity an...