CITI has stopped operations in 2014, to co-launch NOVA LINCS THIS SITE IS NOT BEING UPDATED SINCE 2013
citi banner
  Home  \  Publications  \  InProceedings Page Login  
banner bottom
File Top
Asserting the Correctness of Translations

While building a new language, we assign its semantics by mapping its syntax onto a semantic domain. To do so, we can either (i) do it operationally, by means of small-step morphisms within the same semantic-domain; or (ii) by means of a translation (syntax-to-syntax transformation), onto a target language that has already an operational semantics defined. Despite the fact that it is possible to build the set of syntactic correspondences from a given translation, it is still not clear how we can assert about the correctness of these syntactic correspondences in w.r.t. both the source and target language's underlying semantics. In this paper, we combine the above described techniques by analyzing the translation and establishing a semantic relation between the respective operational semantics, in order to assert the correctness of that translation. We demonstrate our approach with a concrete translation between two languages: State Machines and Petri Nets; and decide about its correctness by using their respective operational semantics as oracles. Finally, we discuss about the validity of our assertions in w.r.t. language translations in general.

@ Proceedings of the 6th Workshop on Multi-paradigm Modeling - MODELS 2011

Publisher: EASST ( Germany )

Date: October, 2011


File Bottom