Bounded exhaustive test input generation from hybrid invariants

ROSNER, NICOLÁS; BENGOLEA, VALERIA; PONZIO, PABLO; SHADI ABDUL KHALEK; AGUIRRE, NAZARENO; FRIAS, MARCELO FABIAN; KHURSHID, SARFRAZ

Portland

Conferencia; ACM International Conference on Object Oriented Programming Systems Languages & Applications, OOPSLA 2014; 2014

Association for Computing Machinery

We present a novel technique for producing bounded exhaus- tive test suites from hybrid invariants, i.e., invariants that are expressed imperatively, declaratively, or as a combination of declarative and imperative predicates. Hybrid specifications are processed using known mechanisms for the imperative and declarative parts, but combined in a way that enables us to exploit information from the declarative side, such as tight bounds computed from the declarative specification, to improve the search both on the imperative and declara- tive sides. Moreover, our technique automatically evaluates different possible ways of processing the imperative side, and the alternative settings (imperative or declarative) for parts of the invariant available both declaratively and imper- atively, to decide the most convenient invariant configuration with respect to efficiency in test generation. This is achieved by transcoping, i.e., by assessing the efficiency of the dif- ferent alternatives on small scopes (where generation times are negligible), and then extrapolating the results to larger scopes.We also show experiments involving collection classes that support the effectiveness of our technique, by demon- strating that (i) bounded exhaustive suites can be computed from hybrid invariants significantly more efficiently than do- ing so using state-of-the-art purely imperative and purely declarative approaches, and (ii) our technique is able to auto- matically determine efficient hybrid invariants, in the sense that they lead to an efficient computation of bounded exhaus- tive suites, using transcoping.