Eclipse Community Forums: TMF (Xtext) » Verifying the correctness of Xtext compiler

Help

Home

Home » Modeling » TMF (Xtext) » Verifying the correctness of Xtext compiler

Show: Today's Messages :: Show Polls :: Message Navigator

Verifying the correctness of Xtext compiler [message #1409928]

Tue, 19 August 2014 10:27

mcse mcse

Messages: 53
Registered: August 2012

Member

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

Report message to a moderator

Re: Verifying the correctness of Xtext compiler [message #1410262 is a reply to message #1409928]

Wed, 20 August 2014 08:37

Christian Dietrich

Messages: 14665
Registered: July 2009

Senior Member

Simply call the generator and compare the result to an expected result ?!? e.g. http://christiandietrich.wordpress.com/2012/05/08/unittesting-xtend-generators/

Twitter : @chrdietrich
Blog : https://www.dietrich-it.de

Report message to a moderator

Re: Verifying the correctness of Xtext compiler [message #1410677 is a reply to message #1410262]

Thu, 21 August 2014 11:12

mcse mcse

Messages: 53
Registered: August 2012

Member

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 ?

Report message to a moderator

Re: Verifying the correctness of Xtext compiler [message #1410687 is a reply to message #1410677]

Thu, 21 August 2014 11:38

Christian Dietrich

Messages: 14665
Registered: July 2009

Senior Member

hi,

i dont get your point so i cannot help

Twitter : @chrdietrich
Blog : https://www.dietrich-it.de

Report message to a moderator

Re: Verifying the correctness of Xtext compiler [message #1410704 is a reply to message #1410687]

Thu, 21 August 2014 12:30

mcse mcse

Messages: 53
Registered: August 2012

Member

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.

Report message to a moderator