Validating Type Checkers Using Property-Based Testing
S. Juhošová (TU Delft - Electrical Engineering, Mathematics and Computer Science)
C.B. Bach Poulsen – Mentor (TU Delft - Programming Languages)
C.R. van der Rest – Graduation committee member (TU Delft - Programming Languages)
K.G. Langendoen – Coach (TU Delft - Embedded Systems)
More Info
expand_more
Codebase
https://gitlab.ewi.tudelft.nl/cse3000-auto-test/typed-expression-generatorsResults
https://gitlab.ewi.tudelft.nl/cse3000-auto-test/sara-resultsOther than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.
Abstract
Manually testing definitional interpreters and their type checkers is a tedious and error-prone process which can largely benefit from automation. This study evaluates the effectiveness of property-based testing on errors in type checkers. Metrics used include the ability to catch different types of errors as well as the ability to provide a good margin of confidence in the results. We define two languages in Haskell and identify properties which should hold for their type checkers. Using a bottom-up approach to expression generation, we evaluate the effectiveness of property-based testing on test suites of type checkers with various types of errors. The method proves to be effective for both the simple and the complex language and manages to catch all defined error types with at least one property to a sufficient degree of confidence. We conclude that property-based testing is an effective tool to help with manual grading of type checkers for definitional interpreters.