5
- 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
property.
- 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
formulae.
- 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.
- 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
specification.
- Explain the notion of correspondence
for behavioral subtypes.
- Show that a stack is a behavioral
subtype of a bag by defining an appropriate
correspondence relation.
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?
slide: Questions
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
eliens@cs.vu.nl
draft version 0.1 (15/7/2001)