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 may 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 (CNF). Second, the test cases are analyzed for ground instances satisfying the premises of the clauses. Particular emphasis is put on the control of test hypothesis’ and test hierarchies to avoid intractability.

We applied our method to several examples, including AVL-trees and the red-black implementation in the standard library from SML/NJ.

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

Please cite this work as follows:
A. D. Brucker and B. Wolff, “Symbolic test case generation for primitive recursive functions,” ETH Zurich, 449, Jun. 2004. Author copy: http://logicalhacking.com/publications/brucker.ea-symbolic-2004/

BibTeX
@TechReport{ brucker.ea:symbolic:2004,
  author      = {Achim D. Brucker and Burkhart Wolff},
  institution = {ETH Zurich},
  language    = {USenglish},
  month       = {jun},
  title       = {Symbolic Test Case Generation for Primitive Recursive
                 Functions},
  areas       = {formal methods, software},
  abstract    = {We present a method for the automatic generation of test
                 cases for HOL formulae containing primitive recursive
                 predicates. These test cases may 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 (CNF). Second, the test cases are
                 analyzed for ground instances satisfying the premises of the
                 clauses. Particular emphasis is put on the control of test
                 hypothesis' and test hierarchies to avoid intractability.
                 
                 We applied our method to several examples, including AVL-trees
                 and the red-black implementation in the standard library from
                 SML/NJ.},
  keywords    = {Symbolic Test Case Generations, Black Box Testing, Theorem
                 Proving, Isabelle/HOL},
  year        = {2004},
  number      = {449},
  num_pages   = {21},
  note        = {Author copy: \url{http://logicalhacking.com/publications/brucker.ea-symbolic-2004/}},
}