Checking software contracts
Richard Mitchell, Ian Maung, John Howse, T. Heathcote · OSTI OAI (U.S. Department of Energy Office of Scientific and Technical Information) · 1995
In object-oriented software, contracts between classes can be expressed in terms of preconditions, postconditions and invariants. In the programming language Eiffel, contracts can be checked at run-time. Within inheritance hierarchies, contracts can be used to control the redefinition of services. In Eiffel, the rules ensure that redefinition is safe in the presence of polymorphism and dynamic binding. This paper shows that Eiffel`s support for contracts can be extended, both to cover the polymorphic case more fully, and to cover other uses of inheritance, including its use for selectively reusing code from a parent class. The paper proposes that software designers should state what properties they claim for any uses of inheritance, in order that extra checks on consistency can be applied, and shows that some extra debugging power could be obtained easily, by changing only the run-time system for Eiffel, rather than the language itself.