We propose a novel general approach for defining expressive type systems for object-oriented languages, based on abstract compilation of programs into coinductive constraint logic programs defined on a specific constraint domain X called type domain. In this way, type checking and type inference amount to resolving a certain goal w.r.t. the coinductive (that is, the greatest) Herbrand model of a logic program (that is, a Horn formula) with constraints over a fixed type domain X. In particular, we show an interesting instantiation where the constraint predicates of X are syntactic equality and subtyping over coinductive object and union types. The corresponding type system is so expressive to allow verification of simple properties like data structure invariants. Finally, we show a prototype implementation, written in Prolog, of the inference engine for coinductive CLP(X), which is parametric in the solver for the type domain X.

Abstract compilation of object-oriented languages into coinductive CLP(X): when type inference meets verification

DAMIANI, Ferruccio
2010-01-01

Abstract

We propose a novel general approach for defining expressive type systems for object-oriented languages, based on abstract compilation of programs into coinductive constraint logic programs defined on a specific constraint domain X called type domain. In this way, type checking and type inference amount to resolving a certain goal w.r.t. the coinductive (that is, the greatest) Herbrand model of a logic program (that is, a Horn formula) with constraints over a fixed type domain X. In particular, we show an interesting instantiation where the constraint predicates of X are syntactic equality and subtyping over coinductive object and union types. The corresponding type system is so expressive to allow verification of simple properties like data structure invariants. Finally, we show a prototype implementation, written in Prolog, of the inference engine for coinductive CLP(X), which is parametric in the solver for the type domain X.
International Conference Formal Verification of Object-Oriented Software 2010
Paris, France
June 28-30, 2010
Formal Verification of Object-Oriented Software. Papers presented at the International Conference, June 28-30, 2010, Paris, France
Fakultät für Informatik (Fak. f. Informatik) Institut für Theoretische Informatik (ITI)
13
330
344
http://digbib.ubka.uni-karlsruhe.de/volltexte/1000019083
Object-oriented languages; coinductive constraint logic programming; Prolog
Davide Ancona; Andrea Corradi; Giovanni Lagorio; Ferruccio Damiani
File in questo prodotto:
Non ci sono file associati a questo prodotto.

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/79880
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact