On Tue, May 08, 2007 at 10:06:32AM +0100, Joel Reymont wrote:

I'm looking for suggestions on how to create invariants for the following AST transformation code. Any suggestions are appreciated!

I asked this question before and Lennart suggested abstract interpretation as a solution. This would require interpreters for both ASTs to determine that the result they achieve is the same. I don't fancy writing a C# interpreter, though, so I'm looking for an easier way out.

Thanks, Joel

You can't claim a translation preserves meaning, if you don't say anything about what C# means. But, you can use a description somebody else already wrote, like the microsoft implementation, or maybe there are formalizations floating around for some theorem provers. For partial specification, checking that a tranformation preserves types is good. If you're translating between languages you can at least define another translation between types, and check that the type of the translation of an expression is the translation of the expressions types. You still need a model of the C# type system, but you shouldn't need to trust the model if you generate code with type annotations, and any missmatches will be caught. You might avoid specifying the meaning of C# directly by instead assuming that certain pairs of expression and translation have the same meaning, whatever that is, and then use some other rules about when two expression in the same langauge are equivalent to stretch your primitive assumptions about translations to the correctness of your whole translation. How you show those rules are correct, I don't know. Brandon.