Computing Publications

Publications Home » A provenly correct Translation of...

A provenly correct Translation of Fickle into Java

Davide Ancona, Christopher Anderson, Ferruccio Damiani, Sophia Drossopoulou, Paola Giannini, Elena Zucca

Journal Article
(ToPLaS) Transactions of Programming Languages ans Systems
Volume 2
2007
ACM
Abstract

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.

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.

PDF of full publication (915 kilobytes)
(need help viewing PDF files?)
BibTEX file for the publication
N.B.
Conditions for downloading publications from this site.
 

pubs.doc.ic.ac.uk: built & maintained by Ashok Argent-Katwala.