Università di Torino
Research on "Formal Methods in Computing"
A provenly correct translation of Fickle into JavaDavide ANCONA, Christopher Anderson, Ferruccio DAMIANI, Sophia DROSSOPOULOU , Paola GIANNINI, and Elena ZUCCA
Work partially supported by DART (IST-2001-33477) and EOS (MIUR Cofin'04)
We present a translation from
allowing objects to
change their class at run-time, into Java.
The translation is provenly correct, in the sense that we
have shown it to preserve the static and dynamic semantics.
Moreover, it is compatible with separate compilation,
the translation of a
class does not depend on the
implementation of used classes.
Based on the formal system, we have developed
The translation turned out to be a more subtle problem
than we expected. In this paper, we discuss four different possible
approaches we considered for the design of the translation and justify our
choice, we present formally the translation and the proof of preservation
of the static and dynamic semantics, and we discuss the prototype
implementation. Moreover, we outline an alternative translation
based on generics that avoids most of the casts (but not all)
needed in the previous translation.
The language Fickle has undergone, and is still
undergoing several phases
of development. In this paper we are discussing the
translation of FickleII.
|Last update: Sep 04, 2008|