A Framework for Testing Object Oriented Software Using Formal Specifications

. In this paper we develop a framework for semi-automated generation of test cases for object oriented programs from formal specifications. We use Object-Z as the formal specification language. We have designed and prototyped a test system called OZTEST. It understands the characteristics of object-oriented specifications including inheritance. OZTEST maps the specification to a corresponding implementation. Test shells generated from the given Object-Z specification are stored as test scripts. OZTEST chooses the test shells to be executed in a particular test-session based on user given criteria. A test class is created by inheriting from the class being tested. The child class thus has all the features of the class being tested, in addition to the routines to test the parent. The results of the test are stored in a file for verification. 1 Introduction Object orientation is a promising method of software engineering. It has provided several features that have enhanced software devel..