Abstract:

Symbolic Test Case Generation for Primitive Recursive Functions

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.