Patent ID: 8046746
Filing Date: 2011-10-25
Classification: G06F

Abstract:
1. A computerized method comprising: receiving a parameterized unit test of an implementation under test; creating, in a computer, at least one axiom summarizing behavior of at least one method of the parameterized unit test, wherein creating a given axiom comprises (a)-(c) for a given method: (a) exploring the given method with a modified one-step relation starting with a variable intensional heap, wherein the variable intensional heap is described by a history of method invocations; and (b) for the modified one-step relation, treating a call to a test statement that checks if an assertion is true as a call to a different test statement that specifies the assertion is assumed true; and (c) whenever a call to the test statement is encountered, generating and conjoining a new axiom formula for further explorations; and symbolically executing the parameterized unit test of the implementation under test to identify one or more execution paths with associated sets of constraints that are generated during symbolic execution, wherein symbolic execution comprises symbolically recording evolving symbolic objects and encapsulated fields with symbolic updates using at least an extensional heap represented by nested applications of an update function, wherein symbolically recording comprises recording with an application of the update function having input parameters comprising a first parameter indicating a previous state of the extensional heap before a present update, a second parameter indicating a symbolic instantiation of a class, a third parameter indicating an identifier of a field in the symbolic instantiation of the class, and a fourth parameter indicating a symbolic value assigned to the field in the symbolic instantiation of the class, wherein the update function operates on a mapping from the encapsulated fields to assigned symbolic values; during symbolic execution of the parameterized unit test, emulating the at least one method of the parameterized unit test by reusing the at least one axiom summarizing behavior of the at least one method of the parameterized unit test based on a textual indication to reuse the at least one axiom summarizing behavior, wherein the at least one axiom summarizing behavior is generated from a previous symbolic execution of a parameterized unit test; from the mapping and the fourth parameter indicating a symbolic value assigned to the field in the symbolic instantiation of the class, creating a test case comprising a concrete assignment to an input parameter of the parameterized unit test; and automatically generating a set of a minimal number of test cases, that includes the created test case, that cover the one or more identified execution paths with associated sets of constraints, that are generated during the symbolic execution, at least by identifying values that solve the associated sets of constraints, that are generated during the symbolic execution, of the identified one or more execution paths of the symbolically executed parameterized unit test; and wherein the variable intensional heap that is described by a history of method invocations is partitioned from the extensional heap of the parameterized unit test for the at least one method that is represented by nested applications of the update function.