Journal article · Conference paper
Effect-driven QuickChecking of compilers
How does one test a language implementation with QuickCheck (aka. property-based testing)? One approach is to generate programs following the grammar of the language. But in a statically-typed language such as OCaml too many of these candidate programs will be rejected as ill-typed by the type checker.
As a refinement Pałka et al. propose to generate programs in a goal-directed, bottom-up reading up of the typing relation. We have written such a generator. However many of the generated programs has output that depend on the evaluation order, which is commonly under-specified in languages such as OCaml, Scheme, C, C++, etc.
In this paper we develop a type and effect system for conservatively detecting evaluation-order dependence and propose its goal-directed reading as a generator of programs that are independent of evaluation order. We illustrate the approach by generating programs to test OCaml's two compiler backends against each other and report on a number of bugs we have found doing so.
Language: | English |
---|---|
Publisher: | Association for Computing Machinery |
Year: | 2017 |
Pages: | 1-23 |
Series: | Proceedings of the Acm on Programming Languages |
ISSN: | 24751421 |
Types: | Journal article and Conference paper |
DOI: | 10.1145/3110259 |
ORCIDs: | Midtgaard, Jan , Nielson, Flemming and Nielson, Hanne Riis |