Universidade Federal de Pernambuco

Lines - Languages and Software Engineering Group

Co-op

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 **R**efinement **O**bject-**o**riented
**L**anguage), 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.

A Weakest Precondition Semantics for Refinament of Object-Oriented Programs

Ana Cavalcanti and David Naumann

Accepted for publication at IEEE Transactions on Software Engineering.