Verifying Test-Hypotheses: An Experiment in Test and Proof

By Achim D. Brucker, 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.

Keywords:
Symbolic Test Case Generations, Black Box Testing, Theorem Proving, Formal Verification, Isabelle/HOL

Please cite this work as follows:
A. D. Brucker, L. Brügger, and B. Wolff, “Verifying test-hypotheses: An experiment in test and proof,” Electronic Notes in Theoretical Computer Science, vol. 220, no. 1, pp. 15–27, 2008, doi: 10.1016/j.entcs.2008.11.003. Proceedings of the Fourth Workshop on Model Based Testing (MBT 2008). Author copy: https://logicalhacking.com/publications/brucker.ea-verifying-2008/

BibTeX
@Article{ brucker.ea:verifying:2008,
  abstract  = {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 \emph{test specification}, is
               partitioned into \emph{test cases} by transformation into a
               normal form called \emph{test theorem}. Second, the test cases
               are analyzed for ground instances (the \emph{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.},
  keywords  = {Symbolic Test Case Generations, Black Box Testing, Theorem
               Proving, Formal Verification, Isabelle/HOL},
  location  = {Budapest, Hungary},
  author    = {Achim D. Brucker and Lukas Br{\"u}gger and Burkhart Wolff},
  journal   = {Electronic Notes in Theoretical Computer Science },
  volume    = {220},
  number    = {1},
  issn      = {1571-0661},
  note      = {Proceedings of the Fourth Workshop on Model Based Testing
               (MBT 2008). 
               Author copy: \url{https://logicalhacking.com/publications/brucker.ea-verifying-2008/}},
  publisher = {Elsevier Science Publishers },
  address   = {Amsterdam },
  language  = {USenglish},
  editor    = {Bernd Finkbeiner and Yuri Gurevich and Alexander K.
               Petrenko},
  title     = {Verifying Test-Hypotheses: An Experiment in Test and Proof},
  pages     = {15--27},
  areas     = {formal methods, software},
  year      = {2008},
  doi       = {10.1016/j.entcs.2008.11.003},
  pdf       = {https://logicalhacking.com/publications/brucker.ea-verifying-2008/brucker.ea-verifying-2008.pdf},
}