topical media & game development

talk show tell print

object-oriented programming

Instructor's Guide: Behavioral Refinement


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.


The verification logic presented in this chapter is based on the notion of observable state changes. The axioms presented abstract from the actual state changes resulting from the execution of a program. The actual behavior of a collection of objects may be modeled by means of a transition system, specifying the execution steps, state changes and observable behavior corresponding to object creation, message passing and instance variable assignments. Such a transition system may be regarded as the operational semantics underlying our assertion logic for objects.

Project assignments

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

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

As a research project one may think of

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


In the final section of this chapter an overview is given of a number of formal approaches to modeling the behavioral properties of collections of objects. This overview is far from complete. For example, not included are the process algebras as described in  [Milner83], which provide a powerful formalism to specify concurrency and communication aspects.
[] readme course(s) preface I 1 2 II 3 4 III 5 6 7 IV 8 9 10 V 11 12 afterthought(s) appendix reference(s) example(s) resource(s) _

(C) Æliens 04/09/2009

You may not copy or print any of this material without explicit permission of the author or the publisher. In case of other copyright issues, contact the author.