Symbolic Test Case Generation for Primitive Recursive Functions

By Achim D. Brucker and Burkhart Wolff.

We present a method for the automatic generation of test cases for HOL formulae containing primitive recursive predicates. These test cases can be used for the animation of specifications as well as for black-box testing of external programs. Our method is two-staged: first, the original formula is partitioned into test cases by transformation into a Horn-clause normal form (HCNF). Second, the test cases are analyzed for instances with constant terms satisfying the premises of the clauses. Particular emphasis is put on the control of test hypotheses and test hierarchies to avoid intractability. We applied our method to several examples, including AVL-trees and the red-black tree implementation in the standard library from SML/NJ.

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

Extended by:
An extended version is available as:
A. D. Brucker and B. Wolff, “Symbolic test case generation for primitive recursive functions,” ETH Zurich, 449, Jun. 2004. Author copy: https://logicalhacking.com/publications/brucker.ea-symbolic-2004/

Please cite this work as follows:
A. D. Brucker and B. Wolff, “Symbolic test case generation for primitive recursive functions,” in Formal approaches to testing of software, J. Grabowski and B. Nielsen, Eds. Heidelberg: Springer-Verlag, 2004, pp. 16–32. doi: 10.1007/b106767. Author copy: https://logicalhacking.com/publications/brucker.ea-symbolic-2005/

BibTeX
@InCollection{ brucker.ea:symbolic:2005,
  abstract   = {We present a method for the automatic generation of test
                cases for HOL formulae containing primitive recursive
                predicates. These test cases can be used for the animation of
                specifications as well as for black-box testing of external
                programs. Our method is two-staged: first, the original
                formula is partitioned into test cases by transformation into
                a Horn-clause normal form (HCNF). Second, the test cases are
                analyzed for instances with constant terms satisfying the
                premises of the clauses. Particular emphasis is put on the
                control of test hypotheses and test hierarchies to avoid
                intractability. We applied our method to several examples,
                including AVL-trees and the red-black tree implementation in
                the standard library from SML/NJ.},
  keywords   = {Symbolic Test Case Generations, Black Box Testing, Theorem
                Proving, Isabelle/HOL},
  location   = {Linz},
  author     = {Achim D. Brucker and Burkhart Wolff},
  booktitle  = {Formal Approaches to Testing of Software},
  language   = {USenglish},
  pages      = {16--32},
  publisher  = {Springer-Verlag },
  address    = {Heidelberg },
  series     = {Lecture Notes in Computer Science },
  number     = {3395},
  isbn       = {3-540-25109-X},
  doi        = {10.1007/b106767},
  editor     = {Jens Grabowski and Brian Nielsen},
  title      = {Symbolic Test Case Generation for Primitive Recursive
                Functions},
  areas      = {formal methods, software},
  extendedby = {brucker.ea:symbolic:2004},
  year       = {2004},
  note       = {Author copy: \url{https://logicalhacking.com/publications/brucker.ea-symbolic-2005/}},
  pdf        = {https://logicalhacking.com/publications/brucker.ea-symbolic-2005/brucker.ea-symbolic-2005.pdf},
}