[Haskell-cafe] QuickCheck invariants for AST transformations

[Brandon Michael Moore]

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.