Skip to main content


Eclipse Community Forums

      Home
Home » Modeling » TMF (Xtext) » Verifying the correctness of Xtext compiler
Verifying the correctness of Xtext compiler [message #1409928] Tue, 19 August 2014 06:27 Go to next message
Eclipse UserFriend
Hi All,

I am looking for building a verifier for my Xtext+Xtend tool that generates a code from another source code. This verifier is expected to guarantee that the code generated by the tool is exactly what is to be generated from the source code.
Do you have any ideas on how to build such a verifier for an Xtext+Xtend tool ?

Thanks
Re: Verifying the correctness of Xtext compiler [message #1410262 is a reply to message #1409928] Wed, 20 August 2014 04:37 Go to previous messageGo to next message
Eclipse UserFriend
Simply call the generator and compare the result to an expected result ?!? e.g. http://christiandietrich.wordpress.com/2012/05/08/unittesting-xtend-generators/
Re: Verifying the correctness of Xtext compiler [message #1410677 is a reply to message #1410262] Thu, 21 August 2014 07:12 Go to previous messageGo to next message
Eclipse UserFriend
Hi Christian,

Thanks a lot for the reply.
The expected result cannot be determined manually for comparison. Instead, there is a number of translation functions, which have already been implemented by the code generator, need to be used. This essentially means that I want to check whether the code generator implemented these functions correctly that always produces the expected result.
Do you have any suggestions on how to ensure the correctness of each function implemented by the code generator ?
Re: Verifying the correctness of Xtext compiler [message #1410687 is a reply to message #1410677] Thu, 21 August 2014 07:38 Go to previous messageGo to next message
Eclipse UserFriend
hi,

i dont get your point so i cannot help
Re: Verifying the correctness of Xtext compiler [message #1410704 is a reply to message #1410687] Thu, 21 August 2014 08:30 Go to previous messageGo to next message
Eclipse UserFriend
I mean that the code generator of my compiler (developed using Xtext and Xtend) includes a set of functions for each grammar rule of the language. These functions are called to translate the elements matched by the grammar rule. However, I need a mechanism that this translation is handled correctly and thus the ultimate translated code from a given specification in the language is as expected. There are solutions that are based on theorem provers, such as coq proof. Therein, the input specification and the translated code are represented in terms of the input language of the coq proof. The coq proof also requires a theorem (and its proof script) that uses the input specification and the translated code, and evaluates to true if they are equivalent. I am just wondering whether there are any other simple solutions that do not require me to use some theorem provers.
Re: Verifying the correctness of Xtext compiler [message #1410729 is a reply to message #1410704] Thu, 21 August 2014 09:26 Go to previous message
Eclipse UserFriend
forget that you use xtend and ask you the question: is there such a solution for pure java. if so you can apply it for xtend as well.
Previous Topic:Avoid outline refresh while editing file
Next Topic:[Eugenia/Xtext] Make the diagram generate formatted code
Goto Forum:
  


Current Time: Sat Sep 20 23:12:04 EDT 2025

Powered by FUDForum. Page generated in 0.07029 seconds
.:: Contact :: Home ::.

Powered by: FUDforum 3.0.2.
Copyright ©2001-2010 FUDforum Bulletin Board Software

Back to the top

Sign up to our Newsletter

A fresh new issue delivered monthly