摘要：In this paper, we present a novel framework TESTAF to support automatic generation and execution of test cases using object-oriented formal specifications. We use IFAD VDM++ as the specification language, but the ideas presented can be applied equally well to other object-oriented formal notations. The TESTAF framework requires a VDM++ specification for a class, a corresponding implementation in C++, and a test specification, to generate and execute test cases, and evaluate the results. The test specification defines valid test sequences in an intermediate specification language based on regular expressions. The framework uses the formal specification of the class, and the test specification to generate empty test shells, which are then filled in with the test data to create concrete test cases. The test data for a method are generated from the input space defined by the method pre condition and the class invariant. The TESTAF applies boundary value analysis strategy to generate the test data. A test driver then executes the implementation with the test data, and uses a conjunction of method post condition and the class invariant as a test oracle to evaluate the results, while reporting failed test cases to the user.
