Specification and verification of object-oriented programs

There is an increasing demand for innovative software that satisfy stringent quality and reliability requirements imposed by users. In recent years Object-Oriented (OO) paradigm is gaining acceptance for developing complex software. The current research so far in OO software engineering is focussed on problem analysis, software design and implementation techniques resulting in a potpourri of representations and procedures. Even though the importance of Verification and Validation (V&V) is known, it has commanded little attention in OO paradigm.;In this thesis we propose a new specification technique called Method and Message Sequence Specification that represents the causal relationship between the instance methods of a set of classes. The Method Sequence Specification (MtSS) of a class documents the correct causal order in which the methods can be invoked at an instance of the class. The Message Sequence Specification (MgSS) of a set of classes documents the causal order in which messages can be sent to instances of different classes. MtSS and MgSS of classes document the message-method interaction and the correct sequence in which messages can flow through a system containing objects.;The importance of specification Consistency and Completeness (C&C) is well known in software engineering. Inconsistency and incompleteness in MtSS and MgSS would lead to faulty design and therefore, C&C of class specification is essential for developing OO design with less faults. In this thesis, we provide a set of rules for developing consistent MtSS and MgSS for both single classes and a set of classes. We also discuss about run time verification system that can ensure that each object is compliant with the corresponding MtSS.;The implementation of a OO design must comply with the design. We propose a new technique of data anomaly detection in OO implementation using MtSS. We then propose several test case generation techniques using MtSS and MgSS that can be used for testing the OO implementation. We then propose "Life Cycle Mutation Testing" that can be used for evaluating the various testing techniques. We also present the results of applying various testing techniques against an example OO program.