Linear refinement is a technique for systematically constructing abstract domains for program analysis directly from a basic domain representing just the property of interest. This paper uses linear refinement to construct a domain for non pair-sharing and freeness analysis. The resulting domain is strictly more precise than the domain for sharing and freeness analysis defined by Jacobs and Langen. Moreover, it can be used for abstract compilation, while Jacobs and Langen's domain can only be used for abstract interpretation. We provide a representation of the domain, together with algorithms for the abstract operations.

We study some properties of SLD-trees related to nite failure. The main results are a theorem stating that the non-ground nite failure set is a correct and fully abstract semantics wrt nite failure and a second theorem stating that the complement of non ground nite failure is andcompositional, i.e. that the nite failure behaviour of conjunctive goals can be derived from the nite failure behaviour of atomic goals. The proofs are based on two new lemmata which generalize to innite derivations theorems which are valid for successful and nitely failed derivations. 1 Introduction The operational semantics of (positive) logic programs is usually based on SLDtrees. Several operational properties, useful for reasoning about programs, can be extracted from an SLD-tree. Examples are SLD-derivations, resultants, partial answers, computed answers, nite failures. All these properties, that we call observables, can be obtained as abstractions of the SLD-tree. The study of the obser...

In this paper we study some first-order formulas, called resultants, which can be used to describe in a concise way most of the relevant information associated to SLD-derivations. We first extend to resultants some classical results of logic programming theory. Then we define a fixpoint semantics for Prolog computed resultants, i.e. those formulas which are obtained by considering the leftmost selection rule. Suitable abstractions of such a semantics are then used to model call patterns and partial answers. Finally we show how these results can be generalized to a larger class of selection rules.

We consider the constraint logic programming paradigm CLP(χ), as defined by Jaffar and Lassez. CLP(χ) integrates a generic computational mechanism based on constraints within the logic programming framework. The paradigm retains the semantic properties of pure logic programs, namely the existence of equivalent operational, model-theoretic and fixpoint semantics. We introduce a framework for defining various semantics, each corresponding to a specific observable property of CLP computations. Each semantics can be defined either operationally (i.e. top-down) or declaratively (i.e. bottom-up). The construction is based on a new notion of interpretation, on a natural extension of the standard notion of model and on the definition of various immediate consequences operators, whose least fixpoints on the lattice of interpretations are models corresponding to various observable properties. We first consider some semantics defined by Jaffar and Lassez and their relations, in terms of correctness and full abstraction, to the equivalences induced on programs by suitable observables. Then we define a fully abstract semantics which models answer constraints. Finally we introduce a semantics for answer constraints which is compositional w.r.t. union of programs. Suitable abstractions of this semantics allow us to obtain correct (in one case fully abstract) semantics for partial answers and call patterns. Our semantic constructions can be taken as the basis for program transformation and (modular) analyses techniques.

In this paper we define a compositional semantics for a generalized composition operator on logic programs. Static and dynamic inheritance as well as composition by union of clauses can all be obtained by specializing the general operator. The semantics is based on the notion of differential programs, logic programs annotated with declarations that establish the programs' external interfaces.

The goal of this paper is to construct a semantic basis for the abstract interpretation of Prolog programs. Prolog is a well-known logic programming language which applies a depth-first search strategy in order to provide a practical approximation of Horn clause logic. While pure logic programming has clean fixpoint, model-theoretic and operational semantics the situation for Prolog is different. Difficulties in capturing the declarative meaning of Prolog programs have led to various semantic definitions which attempt to encode the search strategy in different mathematical frameworks. However, semantic based analyses of Prolog are typically achieved by abstracting the more simple but less precise declarative semantics of pure logic programs. We propose instead to model Prolog control in a simple constraint logic language which is presented together with its declarative and operational semantics. This enables us to maintain the usual approach to declarative semantics of logic programs while capturing control aspects such as search strategy and selection rule.

The theory of abstract interpretation provides a formal framework to develop advanced dataflow analysis tools. The idea is to define a nonstandard semantics which is able to compute, in finite time, an approximated model of the program. In this paper, we define an abstract interpretation framework based on a fixpoint approach to the semantics. This leads to the definition, by means of a suitable set of operators, of an abstract fixpoint characterization of a model associated with the program. Thus, we obtain a specializable abstract framework for bottom-up abstract interpretations of definite logic programs. The specialization of the framework is shown on two examples, namely, gound-dependence analysis and depth-kanalysis.