MODULAR REASONING IN THE PRESENCE OF SUBCLASSING

Considerable progress has been made in understanding how to use subtyp ing in a way that facilitates modular reasoning. However, using subcla ssing in a way that facilitates modular reasoning is not well understo od. Often methods must be overriden as a group because of dependencies on instance variables, and the programmers of subclasses cannot tell which methods are grouped without looking at the code of superclasses. Also, the programmers of subclasses must look at the code of supercla sses to tell what assumptions inherited methods make about the behavio r of overriden methods. We present a systematic way to use subclassing that facilitates formal and informal modular reasoning, Separate spec ifications are given to programmers writing code that manipulates inst ances of a class and to programmers writing subclasses of the class. T he specifications given to programmers of subclasses are divided, by d ivision of labor specifications, into multiple parts. Subclasses may i nherit or override entire parts, but not sub-parts. Reasoning about th e implementation of each part is done independently of other parts.