Davide Ancona, Christopher Anderson, Ferruccio Damiani, Sophia
Drossopoulou, Paola Giannini, and Elena Zucca
A provenly correct translation of
Fickle into Java
Submitted for journal publication
We present a translation from Fickle, a small
object-oriented language
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,
since the translation of a Fickle class does not depend on the
implementation of used classes.
Based on the formal system, we have developed
an implementation.
The translation turned out to be a more subtle problem
than we expected, and the proofs helped us uncover several
subtle errors. 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.
The language Fickle has undergone, and is still
undergoing several phases
of development. In this paper we are discussing the
translation of FickleII.
[ bib |
.html |
.pdf ]
Back
This file has been generated by
bibtex2html 1.43