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@kf8nh.com system administrator [openafs,heimdal,too many hats] allbery@ece.cmu.edu electrical and computer engineering, carnegie mellon university KF8NH