There  has been extensive study of formal type-systems for object-oriented languages, and some study of formal specification, but formalization of development methods  lags behind both the language features and the informal methods presently used. This paper presents a semantic basis for formal development of programs in languages like Java and C++. Our language, called ROOL  (for Refinement  Object-oriented Language), is sufficiently similar to Java to be used in meaningful case studies and to capture some of the central difficulties, yet it is sufficiently constrained to make it possible to give a comprehensible semantics.

We assume the reader is familiar with basic concepts and terminology of object-oriented programming. We address the following challenging issues.

• Dynamic binding of methods means that the version of a method that will be invoked is determined only at run time. Such programs exhibit phenomena similar to higher-order imperative programs.
• Classes are important in practice for modularity, but they are complicated to model (for which reason many studies focus on instance-oriented subtyping).
• Object-oriented programs involve fine-grained control of visibility in terms of private, inherited, and public identifiers.

Our language  has mutually recursive classes and recursive methods. We omit reference types, however. Pointers are ubiquitous in practice, but so are techniques to isolate deliberate sharing from the many situations where value semantics is preferable. Our object values are tuples with recursive nesting but no sharing. We leave pointers as an important but separate issue.

Our long-term aim is to extend to object-oriented programming the most widely-used and well-developed formal methods -- those associated with Hoare logic and weakest preconditions. Because behavioral subclassing involves intermingled programs and specifications, it is natural to extend a refinement calculus. As usual in refinement calculi, our semantics is based on weakest preconditions.

In the approach we adopt, commands denote functions on formulas. In isolation, purely syntactic transformer semantics is dubious. It is our intent to prove operational soundness by relating the weakest precondition semantics presented here to a state transformer semantics of ROOL. At this stage, we have taken the preliminary step of giving a set-theoretic semantics for predicate formulas and expressions. Object states are represented by tuples of attribute values, and in general types denote sets of values. Methods are treated as procedures with a distinguished self parameter. Classes denote tuples of method meanings. Predicate formulas denote sets of states. The interplay between the value-oriented semantics of expressions and the formula-oriented semantics of commands is mediated by the semantics of formulas.

The semantics is based on a typing system. In the methodological literature simpler approaches are usually taken:~there is a fixed global typing, or untyped variables are used and types are treated as predicates. Both approaches are unsuitable for formulating laws about subclasses and inheritance. We employ techniques that have become standard in type theory and denotational semantics; the semantics is defined in terms of typing derivations, which provides convenient access to necessary contextual information.   We do not treat more advanced notions of subtyping than those in Java:~we are interested in reasoning about type casts and tests as they are used in Java and its cousin languages. The typing system is similar  to those used in typing algorithms, where subsumption is incorporated into rules for different constructs rather than being present as a general rule. Nonetheless, soundness of our definitions is not at all obvious, due to subtleties of modelling dynamic binding as well as mutually recursive classes. In this paper, we disallow mutually recursivemethods, which lets us use a simpler, though non-trivial, well-ordering to show that the semantics is well defined.

The main contribution of this paper is the extension of standard weakest precondition semantics to a Java-like language with classes, visibility, dynamic binding, and recursion. We give basic results on soundness of the definitions and discuss notions of program and class refinement.  Our semantics is being used in ongoing research on practical specification and verification.