Principles of Object-Oriented Software Development
[] readme course preface 1 2 3 4 5 6 7 8 9 10 11 12 appendix lectures resources

talk show tell print


This chapter extended the notion of subtyping to include behavioral properties. In section 1, we discussed the interpretation of types as behavior and we looked at the issues involved in preserving invariance and history properties.

Types as behavior


slide: Section 10.1: Types as behavior

Also, we discussed the duality between static and dynamic type constraints. In section 2, a brief characterization of an assertion logic for verifying behavioral properties was given.

Verifying behavioral properties


slide: Section 10.2: Verifying behavioral properties

We looked at a formal characterization of states and state transitions and correctness formulae were introduced as a means to verify the correctness of transitions. We also looked at an axiomatic characterization of the correctness properties of programming language constructs.

On the notion of behavior


  • syntax -- expressions, statements
  • rules -- assignment, object creation, method call
  • compound rules -- composition, conditional, iteration

slide: Section 10.3: On the notion of behavior

In section 3, we looked at how the behavior of an object may be defined in a formal way by means of a transition system. A transition system for an object-based language specifies the rules for assignment, object creation and method call, as well as the computation steps resulting from the evaluation of compound statements.

Objects as behavioral types


  • abstract data types -- representation function
  • correspondence -- abstraction, renaming, extension
  • behavioral subtypes -- correspondence

slide: Section 10.4: Objects as behavioral types

In section 4, it was shown how actual objects may be related to abstract types by means of a representation abstraction function. Further, we discussed explicit guidelines for defining a subtype correspondence relation between behavioral types.

Specifying behavioral compositions


  • global invariants -- dynamic aliasing
  • model-based specification -- state and operations
  • compositions -- contracts, scripts, interaction, joint actions

slide: Section 10.5: Specifying behavioral compositions

Finally, in section 5, we looked at the problems involved in determining global invariants and we discussed what formal means we have available to specify behavioral properties of a collection of objects.


  1. How would you characterize the conformance requirements for subtyping? Explain what properties are involved.
  2. Give an example of signature-compatible types not satisfying the history property.
  3. Explain the duality between imposing constraints statically and dynamically.
  4. How would you formally characterize program states and state transformations?
  5. Explain how you may verify the behavior of a program by means of correctness formulae.
  6. Characterize how the behavior of objects may be modeled by means of a transition system and specify a transition system for a simple object-oriented language.
  7. How would you characterize the relation between an abstract data type and its realizations?
  8. Give an example of an abstract specification of a stack. Define a realization and show that the realization is correct with respect to its abstract specification.
  9. Explain the notion of correspondence for behavioral subtypes.
  10. Show that a stack is a behavioral subtype of a bag by defining an appropriate correspondence relation. What proof obligations must be met?
  11. Discuss the problems involved in satisfying global invariance properties.
  12. What formal methods do you know that deal with specifying the behavior of collections of objects?

slide: Questions

Further reading

As further reading with respect to the verification of programs, I recommend  [AptO] and  [Dahl92]. An assertion logic for a parallel object-oriented language is presented in  [AmBo93].

[] readme course preface 1 2 3 4 5 6 7 8 9 10 11 12 appendix lectures resources

draft version 0.1 (15/7/2001)