Smart Testing of Functional Programs in Isabelle

12 years 3 days ago

Download www21.in.tum.de

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 speciﬁcations in Isabelle. In contrast to naive type-based test data generators, the smart generators take the preconditions into account and only generate tests that fulﬁll 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 signiﬁcantly and enables us to ﬁnd errors in speciﬁcations where naive random and exhaustive testing fail.

Lukas Bulwahn

Real-time Traffic