Assertions for lazy functional languages
Assertions are parts of a program that, instead of contributing to the functionality of the program, express properties of run-time values the programmer expects to hold. It has long been recognised that augmenting programs with assertions improves software quality. An assertion both documents an expected property (e.g. a pre-condition, a post-condition, an invariant) and tests this property at run-time. For example, an assertion may express that the argument of a square root function has to be positive or zero and likewise the result is positive or zero. Assertions can be an attractive alternative to unit tests. Assertions simplify the task of locating the cause of a program fault: in a computation faulty values may be propagated for a long time until they cause an observable error, but assertions can detect such faulty values much earlier.
As long as an assertion does not fail, it should not change the normal observable behaviour of a program.
Lazy functional languages are pure and thus have the advantage that the test of an assertion cannot change program behaviour through side-effects. However, a test may fail to terminate and thus naive assertions result in strict programs and thus a loss of the expressive power of laziness, for example, the use of infinite data structures and cyclic definitions. Hence assertions for a lazy language should be lazy, that is, a property should only be checked for the part of a data structure that is evaluated during the computation anyway.
Papers
-
Monadic
prompt lazy assertions in Haskell.
Olaf Chitil and Frank Huch.
In Zhong Shao, editor, Programming Languages and Systems, 5th Asian
Symposium, APLAS 2007, LNCS 4807, pages 38-53. Springer, November 2007.
-
A pattern
logic for prompt lazy assertions.
Olaf Chitil and Frank Huch.
In Implementation and Application of Functional Languages, 18th
International Workshop, IFL 2006, LNCS 4449, pages 126-144, April 2007.
-
Lazy
assertions.
Olaf Chitil, Dan McNeill, and Colin Runciman.
In Phil Trinder, Greg Michaelson, and Ricardo Pena, editors,
Implementation of Functional Languages: 15th International Workshop, IFL
2003, LNCS 3145. Springer, November 2004.
Software
- MonadicPromptLazyAssertions
-
is a Haskell library for writing assertions that are both prompt and lazy. Properties are formulated in a monadic, parser-combinator-like language. See the APLAS 2007 paper for further information.
