Modular subclass verification: Safely creating correct subclasses without superclass code by Clyde Dwain Ruby (This is the author's Ph.D. dissertation.) Abstract The documentation of object-oriented frameworks and class libraries needs to provide enough information so programmers can reason about the correctness of subclass methods without superclass code. Even though a superclass method satisfies its specification and behaves properly in the context of the superclass itself, a new subclass may cause that method to have unexpected or unverifiable behavior. For example, inherited superclass code can call down to subclass methods which may cause a superclass method to no longer satisfy its specification. Furthermore, without superclass code, downcalls can result in unverifiable side-effects. Aliasing can also result in unexpected or unverifiable side-effects. In this dissertation, we present a reasoning technique that allows programmers, who have no access to superclass code, to avoid the problems caused by downcalls and aliasing. The rules use the specification of the abstract data representation of a class and the frame axiom of each method to determine when a method override is necessary and when verifiers can safely reason about the behavior of super-calls. We describe a type system and propose a tool that would warn when a super-call is unsafe or when a superclass method needs to be overridden. A verification logic is also presented and proved sound. The verification logic is based on specifications given in the Java Modeling Language (JML) and uses superclass and subclass specifications to modularly verify the correctness of subclass code. A set of guidelines is proposed for class library implementers that, if followed, guarantees that superclass methods will always be safe to call and that our verification logic can safely be used. These guidelines make our technique easy to use in practice. Keywords: Downcalls, super-calls, subclass, semantic fragile subclassing problem, subclassing contract, code contract, specification inheritance, method refinement, alias control, specification of side effects, Java language, JML language. 2006 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, validation, tools, JML; D.2.7 [Software Engineering] Distribution, Maintenance, and Enhancement -- Documentation, extensibility; D.2.10 [Software Engineering] Design -- Methodologies, tools, JML; D.2.11 [Software Engineering] Software Architectures -- Data abstraction, information hiding, languages, JML; 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.