topical media & game development
This chapter extended the notion of
subtyping to include
In section 1,
we discussed the interpretation of types
as behavior and we looked at
the issues involved in preserving
invariance and history properties.
- subtype requirements -- preservation of behavioral properties
- behavioral properties -- invariance, history
- duality -- static versus dynamic constraints
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
- 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
- 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.
- 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.
- 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.
- How would you characterize the conformance
requirements for subtyping?
Explain what properties are involved.
- Give an example of signature-compatible
types not satisfying the history
- Explain the duality between imposing
constraints statically and dynamically.
- How would you formally characterize
program states and state transformations?
- Explain how you may verify the behavior
of a program by means of correctness
- Characterize how the behavior of objects
may be modeled by means of a transition
specify a transition system for a simple
- How would you characterize
the relation between an abstract data type
and its realizations?
- 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
- Explain the notion of correspondence
for behavioral subtypes.
- Show that a stack is a behavioral
subtype of a bag by defining an appropriate
What proof obligations must be met?
- Discuss the problems involved
in satisfying global invariance properties.
- What formal methods do you know
that deal with specifying the behavior of
collections of objects?
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].
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.