Safe Object-Oriented Software: The Verified Design-By-Contract Paradigm

摘要

In recent years, large sectors of the software development industry have moved from the procedural style of software development to an object-oriented style. Safety-critical software developers have largely resisted this trend because of concerns about verifiability of object-oriented systems. This paper outlines the benefits offered by object technology and considers the key features of the object-oriented approach from a user's perspective. We review the main issues affecting safety and propose a paradigm - Verified Design-by-Contract - that uses formal methods to facilitate the safe use of inheritance, polymorphism, dynamic binding and other features of the object-oriented approach. An outline of Perfect Developer - a tool supporting the Verified Design-by-contract paradigm - is included.