An abstract model for
constraint logic programming
languages
Niels Jørgensen
Abstract
The model CLP(X)(pat) is proposed as a tool for a certain class of dataflow analyses of CLP languages: analyses which are defined in terms of call and success patterns. The model is defined using Marriott, Søndergaard, and Jones' theory of denotational abstract interpretation of logic programs. In the model's semantic definition for standard interpretation of CLP languages, the input and output of clauses consists of sets of constrained atoms, that is, of atom-constraint pairs. In the non-standard interpretation of a CLP program, a call or success pattern is a description of such a set.
Two well-known groundness analyses are re-formulated within the framework. The analyses use propositional formulas to describe the groundness of program variables.
The simplest one uses formulas that are conjunctions of variables, and the more refined is the pos
analysis which employs arbitrary, so-called positive propositional formulas.
It can be observed that while many early analyses of Prolog were stated in terms of call and success patterns, the use of patterns has declined in recent years, especially in research were emphasis is on formal justification of correctness.
On the basis of the two example analyses, we argue that call and success patterns may provide a venue to more intuitive analyses, while retaining a sound, formal basis, and so perhaps they deserve a come-back into the field of abstract interpretation of Prolog and other CLP languages.