Sciweavers

Share
ENTCS
2008

Verifying Test-Hypotheses: An Experiment in Test and Proof

8 years 12 months ago
Verifying Test-Hypotheses: An Experiment in Test and Proof
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. Test data were used in an automatically generated test-driver running the program under test. 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 a validation by test and a validation 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.
Achim D. Brucker, Lukas Brügger, Burkhart Wol
Added 10 Dec 2010
Updated 10 Dec 2010
Type Journal
Year 2008
Where ENTCS
Authors Achim D. Brucker, Lukas Brügger, Burkhart Wolff
Comments (0)
books