Æliens

This chapter extends the notion of subtyping to include behavioral properties. It discusses the interpretation of types as behavior and introduces an assertion logic for verifying behavioral properties. A brief introduction is given to the operational semantics underlying the verification logic. We then look at the interpretation of objects as behavioral types, and present guidelines for designing subtypes satisfying behavioral constraints. Finally, we discuss what formal means we have available to specify the behavioral properties of a collection of related objects.

There is still a need to incorporate the theoretical insights with respect to the semantics and proof theory of object-oriented languages in practical development methods. As assignments that hint towards the integration of theory one may think of

• providing a proof theory for a subset of C++
• developing an operational semantics for a subset of C++
• formulating guidelines for safe inheritance in Smalltalk, Eiffel, C++ or Java

Naturally, for student assignments an exploratory study is probably the most one can ask for.

As a research project one may think of

• the development of an object-oriented model-based specification formalism

that allows for an easy transition from a specification to an implementation in some object-oriented language.