A test class framework for generating test cases from Z specifications

This paper introduces test classes and a test class framework for generating test cases from Z specifications. We define a test class using object-oriented concept in test framework instead of Phil Stock´s test template. Our test framework for Z specifications uniformly defines the test data and oracles in a test class that also contains the information of before states and after states for an operation. Thus, the derivation and construction of test case and test sequence information can be unified in a test framework. We present an example to demonstrate how to generate test cases using the test framework. To support the framework, we have designed and implemented a test case generation system, TCGS, and its functions are briefly described in the paper