Safely creating correct subclasses without seeing superclass code

A major problem for object-oriented frameworks and class libraries is how t o provide enough information about a superclass, so programmers can safely create new subclasses without giving away the superclass's code. Code inher ited from the superclass can call down to methods of the subclass, which ma y cause nontermination or unexpected behavior. We describe a reasoning tech nique that allows programmers, who have no access to the code of the superc lass, to determine both how to safely override the superclass's methods and when it is safe to call them. The technique consists of a set of rules and some new forms of specification. Part of the specification would be genera ted automatically by a tool, a prototype of which is planned for the formal specification language JML. We give an example to show the kinds of proble ms caused by method overrides and how our technique can be used to avoid th em. We also argue why the technique is sound and give guidelines for librar y providers and programmers that greatly simplify reasoning about how to av oid problems caused by method overrides.