TY  - CHAP
AU  - Brucker, Achim D.
AU  - Wolff, Burkhart
ED  - Grabowski, Jens
ED  - Nielsen, Brian
PY  - 2004//
TI  - Symbolic Test Case Generation for Primitive Recursive Functions
BT  - Formal Approaches to Testing of Software
T3  - Lecture Notes in Computer Science
SP  - 16
EP  - 32
IS  - 3395
PB  - Springer-Verlag
CY  - Heidelberg
KW  - symbolic test case generations, black box testing, theorem proving, Isabelle/HOL 
N2  - 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. 
SN  - 3-540-25109-X
UR  - http://www.brucker.ch/bibliography/abstract/brucker.ea-symbolic-2005
L1  - http://www.brucker.ch/bibliography/download/2005/brucker.ea-symbolic-2005.pdf
UR  - http://dx.doi.org/10.1007/b106767
ID  - brucker.ea:symbolic:2005
ER  -