Specification and Verification Techniques of Object Oriented Programs using Invariants

摘要

The consistency and correctness of object oriented programs greatly rely on the extent to which object invariants hold. But while dealing with object invariants there are many related issues that need to be addressed to ensure a completely reliable object oriented software. These issues include ownership transfer, sub-classing, dynamic binding and modular reasoning. A lot of work has been done in the last decade on improving the consistency of object oriented softwares using object invariants and class invariants. A detailed analysis of all the modern approaches and their contribution in improving the specification and verification techniques has been given in this paper.