Abstract:


Verifying Test-Hypotheses: An Experiment in 
Test and Proof



Achim D. Brucker and Lukas Brügger and 
Burkhart Wolff



HOL-TestGen is a specification and test case generation 
environment extending the interactive theorem prover 
Isabelle/HOL. The HOL-TestGen method is two-staged: 
first, the original formula, called test specification, 
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.As such, 
explicit test hypotheses establish a logical link between 
validation by test and by proof. Since HOL-TestGen generates 
explicit test hypotheses and makes them amenable to formal 
proof, the system is in a unique position to explore the 
relations between them at an example.