This document is an extended abstract of ongoing work on reasoning about correctness and behavioral subclassing for programs using some of the challenging features of   Java. We include dynamic binding and inheritance, visibility control, and mutually recursive classes and recursive methods (but not pointers or concurrency). We have already given a  predicate-transformer semantics for a language with these features as well as specification constructs from refinement calculi. Here we discuss intrinsic notions of behavioral subclassing and refinement, and we discuss soundness of proof by forward simulation.

Our long-term goal is to use refinement laws as the basis both for a development method and for tools supporting program analysis, verification, and compilation. In our current project the focus is on semantics, behavioral subclassing and refinement, and laws of refinement that are sufficient to reduce programs to a normal form. Laws, however, are beyond the scope of this abstract.

For stepwise development of object-oriented programs, one needs a notion of refinement to account for correctness-preserving replacement of one definition of a class by another. Adequate formalization of refinement depends on language features used in programs and specifications. Unbridled type tests and casts can thwart behavioral subclassing because their semantics is based on naming.  By making a careful study of behavioral refinement in a language with many of the challenging features of Java, we believe we will contribute to the advance of formal techniques for analysis and verification of Java programs.

Our results shed light on issues relevant beyond the relatively narrow and long-term goals of program development based on refinement. In particular, our  semantic model can illuminate issues that are obscured in detailed operational models, just as other abstractions ---Hoare logic, coalgebras, and monads--- are useful conceptual tools.