Reasoning and refinement in object-oriented specification languages

Abstract

This paper describes a formal object-oriented specification language, Z++, and identifies proof rules and associated specification structuring and development styles for the facilitation of validation and verification of implementations against specifications in this language. We give inference rules for showing that certain forms of inheritance lead to refinement, and for showing that refinements are preserved by constructs such as promotion of an operation from a supplier class to a client class. Extension of these rules to other languages is also discussed.