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

SPOTO, Nicola Fausto
2002

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.
static analysis; abstract interpretation; logic programs
File in questo prodotto:
File Dimensione Formato  
GeneralizingDefPos.pdf

solo utenti autorizzati

Tipologia: Versione dell'editore
Licenza: Accesso ristretto
Dimensione 598.2 kB
Formato Adobe PDF
598.2 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/11562/16663
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 4
  • ???jsp.display-item.citation.isi??? 3
social impact