Smart Testing of Functional Programs in Isabelle
| Autor: | Lukas Bulwahn |
|---|---|
| Rok vydání: | 2012 |
| Předmět: |
Functional programming
Horn clause Theoretical computer science Generator (computer programming) Programming language Test data generation Computer science Proof assistant computer.software_genre TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Haskell Compiler computer computer.programming_language Test data |
| Zdroj: | Logic for Programming, Artificial Intelligence, and Reasoning ISBN: 9783642287169 LPAR |
| DOI: | 10.1007/978-3-642-28717-6_14 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|