Andrew Coppin wrote:
Here is a *much* bigger problem: How do you check that an interpretter is correct??
Before checking for correctness, you have to define correctness. What is the specification of your interpreter?
You can't very easily write a QuickCheck property that will generate every possible valid expression and then check that the output of the interpretter is formally equivilent. The QuickCheck property would be a second copy of the interpretter, which proves nothing!
Well, if you have two *different* interpreters, that would at least reassure you somewhat. Consider a naive substituation-based interpreter and a clever environment-based interpreter. The former is often easier to write and easier to get correct, and the latter is often what you want in the end. Since you seem to be implementing a standard language, you could use an existing implementation to check against. many lambda calculus style languages can easily be transformed into scheme, for example.
Any hints? Just how *do* you check something large like this?
You could write a lot of test cases, calculating the correct answers by hand. You could check that during evaluation, you have always wellformed terms (e.g. evaluation does not introduce new free variables). You could even check that after evaluation stops, you have indeed a normal form. You could try to check the components of your interpreter (e.g. environment lookup, term substituation, simplification) independently. Tillmann