Incremental reasoning for object oriented systems

Abstract

Inheritance and polymorphism are key mechanisms of the object-oriented approach that enable designers to develop systems in an incremental manner. In this paper, we develop techniques for reasoning incrementally about the behavior of such systems. A derived class designer will be able, using the proposed approach, to arrive at the richer behavior that polymorphic methods inherited from the base class will exhibit in the derived class, without reanalyzing the code bodies of these methods. The approach is illustrated by applying it to a simple case study. © Springer-Verlag Berlin Heidelberg 2004.