[Haskell-cafe] Compiler's bane
Brandon S. Allbery KF8NH
allbery at ece.cmu.edu
Mon Sep 1 23:18:14 EDT 2008
On 2008 Sep 1, at 20:06, Tillmann Rendel wrote:
> Andrew Coppin wrote:
>> 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.
You can define a set of valid transformations, have the interpreter
log each transformation, and verify that all are correct (that is,
that both the transformation and the logged result are correct.
This assumes the interpreter can be resolved down to a sufficiently
simple set of transformations; if not, you're right back at having the
tester being the interpreter itself. Note that you don't check if the
transformation plan for the program matches a specified list, just
that all transformations are correct. (Just remember that "logic is
an organized way of going wrong with confidence.")
brandon s. allbery [solaris,freebsd,perl,pugs,haskell] allbery at kf8nh.com
system administrator [openafs,heimdal,too many hats] allbery at ece.cmu.edu
electrical and computer engineering, carnegie mellon university KF8NH
More information about the Haskell-Cafe