Modularity and the Rule of Adaptation

This paper presents a new rule for reasoning about method calls in object-oriented programs. It is an adaptation of Hoare's rule of adaptation to the object-oriented paradigm, which takes both the write effects and the creational effects of a method into account. The new rule contributes in various ways to the modularity of the specification. We also argue that our rule of adaptation is the missing link between Hoare logics and proof outlines for object-oriented programs.

• Type: Conference
• Year: 2004
• Where: AMAST
• Authors: Cees Pierik, Frank S. de Boer
• Keywords: AMAST 2004, Hoare's Rule, Object-oriented Paradigm, Object-oriented Programs, Software Engineering