This paper is concerned with the type analysis of logic programs where, by type, we mean a property closed under instantiation. We define a chain of abstractions from Herbrand constraints to logical formulas via the set of their solutions. Every step of the chain is an instance of abstract interpretation. The use of logical formulas for type analysis is a generalisation of the traditional Boolean domains Def and Pos for groundness analysis. In this context, implication is the logical counterpart of the use of linear refinement. While logical formulas can sometime be used for an actual implementation of our domains, in the general case they are infinite objects. Therefore, we apply a final abstraction from possibly infinite logical formulas to (finite) logic programs. Thus, logic programs are themselves used for the type analysis of logic programs. The advantage of our technique with respect to the many frameworks for type analysis present in the literature is that we have developed our domains by using the formal techniques of abstract interpretation and linear refinement. Therefore, their construction is guided by the underlying theory, from which their properties are derived.

Generalising Def and Pos to Type Analysis

Abstract

This paper is concerned with the type analysis of logic programs where, by type, we mean a property closed under instantiation. We define a chain of abstractions from Herbrand constraints to logical formulas via the set of their solutions. Every step of the chain is an instance of abstract interpretation. The use of logical formulas for type analysis is a generalisation of the traditional Boolean domains Def and Pos for groundness analysis. In this context, implication is the logical counterpart of the use of linear refinement. While logical formulas can sometime be used for an actual implementation of our domains, in the general case they are infinite objects. Therefore, we apply a final abstraction from possibly infinite logical formulas to (finite) logic programs. Thus, logic programs are themselves used for the type analysis of logic programs. The advantage of our technique with respect to the many frameworks for type analysis present in the literature is that we have developed our domains by using the formal techniques of abstract interpretation and linear refinement. Therefore, their construction is guided by the underlying theory, from which their properties are derived.
Scheda breve Scheda completa Scheda completa (DC)
2002
static analysis; abstract interpretation; logic programs
File in questo prodotto:
File
GeneralizingDefPos.pdf

solo utenti autorizzati

Tipologia: Versione dell'editore
Licenza: Accesso ristretto
Dimensione 598.2 kB
Utilizza questo identificativo per citare o creare un link a questo documento: `https://hdl.handle.net/11562/16663`