Reasoning about polymorphic behavior

The standard approach to dealing with OO polymorphism is to require subclasses to be behavioral subtypes of the base class. This ensures that reasoning that has been done about any client code that operates on base class objects will continue to be valid if instances of the subclasses are used in place of the base class objects. But often one is interested in stronger properties of the client code, in particular that its behavior will be appropriate to the specific subclass objects that are used, rather than just generic behavior that ignores the differences between the different subclasses. The authors present some examples to illustrate the problem, and propose a method of reasoning that allows one to establish stronger properties of the client code on the basis of the richer behavior provided by the appropriate derived classes