An abstract interpretation framework to reason on finite failure and other properties of finite and infinite computations

摘要

We extend the framework of Comini et al. (Inform. Comput. (1999), to appear) in order to be able to reason on properties (of abstractions) of possibly infinite SLD-derivations. This issue is relevant since some important operational properties such as finite failure, infinite behavior can only be addressed as abstraction of finite and infinite SLD-derivations. The framework allows us to define new fixpoint semantics correctly modelling such properties and address problems such as compositionality w.r.t. various syntactic operators, correctness and minimality of the chosen denotations. In this paper we also apply the framework in order to obtain a new fixpoint semantics, based on a co-continuous operator, which correctly models finite failure and is compositional w.r.t. the syntactic operators.