A Framework for Inheritance Testing from VDM++ Specifications

The benefits offered by the use of formal methods are not limited to avoidance of specification errors and elimination of ambiguities only - a formal specification also provides a sound basis for generating test suites. Inheritance is a powerful mechanism in object-oriented paradigm by which a subclass inherits data and functionality of a super class. Testing of inheritance relationships is crucial in object-oriented testing, as an inheritance error may lead to subtle bugs such as due to overridden functionality. In this paper, we introduce a technique to generate test cases for inheritance testing, using a VDM++ formal specification. The proposed technique is based on the flattening of a VDM++ specification class, and then generating operation sequences from the trace structure specified in the VDM++ specification. The input space for each operation is partitioned, and a test model is constructed from the operation sequences and the input partitions. Test paths are generated from the test model, which cover the different operation sequences as well as the partitions. We also define various coverage criteria for test path generation