We use abstract interpretation to abstract a compositional trace semantics for a simple imperative object-oriented language into its projection over a set of program points called watchpoints. We say that the resulting watchpoint semantics is focused on the watchpoints. Every abstraction of the computational domain of this semantics induces an abstract, still compositional and focused watchpoint semantics. This establishes a basis for developing static analyses obtaining information pertaining only to the watchpoints. As an example, we consider three domains for class analysis of object-oriented programs derived from three techniques present in the literature viz. rapid type analysis, a simple dataflow analysis and a constraint-based analysis. We obtain three static analyses which are provably correct and whose abstract operations are provably optimal. Moreover, we prove that our formalisation of the constraint-based analysis is more precise than that of the other two analyses. We have implemented our watchpoint semantics and our three domains for class analysis. This implementation shows that the time and space costs of the analysis are actually proportional to the number of watchpoints, as a consequence of the focused nature of the watchpoint semantics.

Class Analyses as Abstract Interpretations of Trace Semantics

SPOTO, Nicola Fausto;
2003

Abstract

We use abstract interpretation to abstract a compositional trace semantics for a simple imperative object-oriented language into its projection over a set of program points called watchpoints. We say that the resulting watchpoint semantics is focused on the watchpoints. Every abstraction of the computational domain of this semantics induces an abstract, still compositional and focused watchpoint semantics. This establishes a basis for developing static analyses obtaining information pertaining only to the watchpoints. As an example, we consider three domains for class analysis of object-oriented programs derived from three techniques present in the literature viz. rapid type analysis, a simple dataflow analysis and a constraint-based analysis. We obtain three static analyses which are provably correct and whose abstract operations are provably optimal. Moreover, we prove that our formalisation of the constraint-based analysis is more precise than that of the other two analyses. We have implemented our watchpoint semantics and our three domains for class analysis. This implementation shows that the time and space costs of the analysis are actually proportional to the number of watchpoints, as a consequence of the focused nature of the watchpoint semantics.
class analysis; static analysis; denotational semantics; abstract interpretation
File in questo prodotto:
File Dimensione Formato  
ClassAnalysesAsAbstractInterpretation.pdf

solo utenti autorizzati

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