Builders Usage in Automated Test Case Generation

As discussed in the article, the API of BinaryTree has 6 methods (including a single constructor), and our approach automatically identified that the constructor plus the add method are sufficient and minimal builders for BinaryTree.

Using the full API we could define the driver program in the left figure below, to build inputs (BinaryTree objects) for the verification of the add method using the Java PathFinder software model checker. Notice that, as we don't know what the builders are, without a thorough inspection of the BinaryTree code, we have to build a naive driver that employs all the methods in the API to build the inputs. In contrast, knowing that the constructor and add methods are a sufficient set of builders, we can create the more succinct and efficient driver program shown in the right figure below.

Preliminary experimental results

We ran both programs above using the Java PathFinder software model checker, that allow to execute at most seven methods (see variable bound) to build inputs for the add call after the loop. Therefore, we check that add works well when invoked with BinaryTree instances with at most seven nodes, containing integers from 0 to 6 as keys.

The JPF runtime results using the "whole API" driver program on the left are below:

elapsed time: 00:03:47

max memory: 3189MB

The JPF runtime results using the "builders only" driver program on the right are below:

elapsed time: 00:00:35

max memory: 1637MB

This shows that automated builders identification can help in suggesting the methods that can be used to define more efficient drivers in bounded model checking.

Newer preliminary results showed that the payoff of using builders only is bigger as the scope grows (number of nodes, number of integers to use as keys).

Experimental results for the remaining case studies, involving many scopes will be added soon.