We apply the methodology of domain refinement to systematically derive domains for type analysis. Domains are built by iterative application of the Heyting completion operator to a given set of basic types. We give a condition on the type system which assures that two steps of iteration are sufficient to reach the fixpoint. Moreover, we provide a general representation for type domains through transfinite formulas. Finally, we show a subset of finite formulas which can be used as a computationally feasible implementation of the domains and we define the corresponding abstract operators.

An Experiment in Domain Refinement: Type Domains and Type Representations for Logic Programs

SPOTO, Nicola Fausto
1998

Abstract

We apply the methodology of domain refinement to systematically derive domains for type analysis. Domains are built by iterative application of the Heyting completion operator to a given set of basic types. We give a condition on the type system which assures that two steps of iteration are sufficient to reach the fixpoint. Moreover, we provide a general representation for type domains through transfinite formulas. Finally, we show a subset of finite formulas which can be used as a computationally feasible implementation of the domains and we define the corresponding abstract operators.
static analysis; abstract interpretation; linear refinement
File in questo prodotto:
File Dimensione Formato  
An-experiment-in-domain-refinement.pdf

solo utenti autorizzati

Tipologia: Versione dell'editore
Licenza: Accesso ristretto
Dimensione 1.08 MB
Formato Adobe PDF
1.08 MB 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/16675
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 11
  • ???jsp.display-item.citation.isi??? ND
social impact