Università di Torino

Research on "Formal Methods in Computing"

A provenly correct translation of Fickle into Java

Davide 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)

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. The language Fickle has undergone, and is still undergoing several phases of development. In this paper we are discussing the translation of FickleII.

The documents distributed by this server have been provided by the contributing authors as a means to ensure timely dissemination of scholarly and technical work on a noncommercial basis. Copyright and all rights therein are maintained by the authors or by other copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.


author    = {Davide Ancona and Christopher Anderson and Ferruccio Damiani and Sophia Drossopoulou and Paola Giannini and Elena Zucca},
title     = {A provenly correct translation of Fickle into Java},
journal   = {ACM Transactions On Programming Languages and Systems},           
year      = {2007},
volume    = {29},                                                              
number    = {2},                                                               
pages     = {Article No. 13 (67 pages)},                                
publisher = {ACM},                                                             
url = {http://www.di.unito.it/~damiani/papers/toplas3.html}                     

["Formal Methods in Computing" group] [Department's HOME]

Last update: Sep 04, 2008