This paper further investigates the potential and practical applicability of abstract compilation in two different directions. First, we formally define an abstract compilation scheme for precise prediction of uncaught exceptions for a simple Java-like language; besides the usual user declared checked exceptions, the analysis covers the runtime ClassCastException. Second, we present a general implementation schema for abstract compilation based on coinductive CLP with variance annotation of user-defined predicates, and propose an implementation based on a Prolog prototype meta-interpreter, parametric in the solver for the subtyping constraints.

Abstract compilation of object-oriented languages into coinductive CLP(X): can type inference meet verification?

DAMIANI, Ferruccio
2011-01-01

Abstract

This paper further investigates the potential and practical applicability of abstract compilation in two different directions. First, we formally define an abstract compilation scheme for precise prediction of uncaught exceptions for a simple Java-like language; besides the usual user declared checked exceptions, the analysis covers the runtime ClassCastException. Second, we present a general implementation schema for abstract compilation based on coinductive CLP with variance annotation of user-defined predicates, and propose an implementation based on a Prolog prototype meta-interpreter, parametric in the solver for the subtyping constraints.
Formal Verification of Object-Oriented Software - International Conference, FoVeOOS 2010, Paris, France, June 28-30, 2010, Revised Selected Papers
Springer-Verlag
LECTURE NOTES IN COMPUTER SCIENCE
6528
31
45
9783642180699
9783642180705
http://www.springer.com/computer/swe/book/978-3-642-18069-9
http://www.springerlink.com/content/t25jq107744016gn/
Java - formal verification - microkernel - object orientation - object-oriented languages - program verification - type inference
Davide Ancona; Andrea Corradi; Giovanni Lagorio; Ferruccio Damiani
File in questo prodotto:
File Dimensione Formato  
LNCS-post-foveoos10-2011.pdf

Accesso riservato

Tipo di file: POSTPRINT (VERSIONE FINALE DELL’AUTORE)
Dimensione 278.45 kB
Formato Adobe PDF
278.45 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: https://hdl.handle.net/2318/81714
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 11
  • ???jsp.display-item.citation.isi??? 4
social impact