On theorem prover-based testing
Achim D. Brucker, Burkhart Wolff · Formal Aspects of Computing · 2012
Abstract HOL -TestGen is a specification and test case generation environment extending the interactive theorem prover Isabelle/ HOL . As such, Testgen allows for an integrated workflow supporting interactive theorem proving, test case generation, and test data generation. The HOL -TestGen method is two-staged: first, the original formula is partitioned into test cases by transformation into a normal form called test theorem . Second, the test cases are analyzed for ground instances (the test data ) satisfying the constraints of the test cases. Particular emphasis is put on the control of explicit test-hypotheses which can be proven over concrete programs. Due to the generality of the underlying framework, our system can be used for black-box unit, sequence, reactive sequence and white-box test scenarios. Although based on particularly clean theoretical foundations, the system can be applied for substantial case-studies.