[Haskell-cafe] Compiler's bane
rendel at daimi.au.dk
Mon Sep 1 20:06:21 EDT 2008
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
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.
More information about the Haskell-Cafe