Safely Creating Correct Subclasses without Seeing Superclass Code by Clyde Ruby and Gary T. Leavens Abstract A major problem for object-oriented frameworks and class libraries is how to provide enough information about a superclass, so programmers can safely create new subclasses without giving away the superclass's code. Code inherited from the superclass can call down to methods of the subclass, which may cause nontermination or unexpected behavior. We describe a reasoning technique that allows programmers, who have no access to the code of the superclass, 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 generated 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 problems caused by method overrides and how our technique can be used to avoid them. We also argue why the technique is sound and give guidelines for library providers and programmers that greatly simplify reasoning about how to avoid problems caused by method overrides. Keywords: Downcalls, subclass, semantic fragile subclassing problem, subclassing contract, specification inheritance, method refinement, Java language, JML language. 1999 CR Categories: D.2.1 [Software Engineering] Requirements/Specifications --- languages, tools, JML; D.2.2 [Software Engineering] Design Tools and Techniques --- Object-oriented design methods, software libraries; D.2.3 [Software Engineering] Coding Tools and Techniques --- Object-oriented programming; D.2.4 [Software Engineering] Software/Program Verification --- Class invariants, correctness proofs, formal methods, programming by contract, reliability, tools, JML; D.2.7 [Software Engineering] Distribution, Maintenance, and Enhancement --- Documentation, Restructuring, reverse engineering, and reengineering; D.2.13 [Software Engineering] Reusable Software --- Reusable libraries; D.3.2 [Programming Languages] Language Classifications --- Object-oriented langauges; D.3.3 [Programming Languages] Language Constructs and Features --- classes and objects, frameworks, inheritance; F.3.1 [Logics and Meanings of Programs] Specifying and Verifying and Reasoning about Programs --- Assertions, invariants, logics of programs, pre- and post-conditions, specification techniques; Copyright (c) 2000 by Clyde Ruby and Gary T. Leavens.