topical media & game development

talk show tell print

object-oriented programming

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


  • states -- transformations
  • verification -- correctness formulae
  • axioms -- consequence rules, abstraction

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.

(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.