- 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