Smart Testing of Functional Programs in Isabelle

7 years 6 months ago
Smart Testing of Functional Programs in Isabelle
Abstract. We present a novel counterexample generator for the interactive theorem prover Isabelle based on a compiler that synthesizes test data generators for functional programming languages (e.g. ML, Haskell) from specifications in Isabelle. In contrast to naive type-based test data generators, the smart generators take the preconditions into account and only generate tests that fulfill the preconditions. The smart generators are constructed by a compiler that reformulates the preconditions as logic programs and analyzes them with an enriched mode inference. From this inference, the compiler can construct the desired generators in the functional programming language. Applying these test data generators reduces the number of tests significantly and enables us to find errors in specifications where naive random and exhaustive testing fail.
Lukas Bulwahn
Added 25 Apr 2012
Updated 25 Apr 2012
Type Journal
Year 2012
Where LPAR
Authors Lukas Bulwahn
Comments (0)