An Integrated Approach to Assertion-Based Random Testing

Slides

We present an approach and tool for assertion-based random testing of Horn clauses programs that is integrated within an overall assertion-based development model. Our starting point is the Ciao assertion model, a framework that unifies unit testing and run-time verification, as well as static verification and static debugging, using a common assertion language. In this context, the idea of generating random test values from assertion preconditions emerges naturally since these preconditions are conjunctions of literals, and the corresponding predicates can in principle be used as generators. Our tool generates valid inputs from the properties that appear in the assertions shared with other parts of the model, and the run time-check instrumentation of the Ciao framework is used to perform a wide variety of checks. This integration also facilitates the combination with static analysis. The generation process is based on running standard predicates under random search strategies. We propose methods for supporting constraints and other (C)LP-specific properties, including combinations of shape-based (regular) types and variable sharing and instantiation, and we also provide some ideas for shrinking for these properties.