Æliens

1

• subtype requirements -- preservation of behavioral properties
• behavioral properties -- invariance, history
• duality -- static versus dynamic constraints

2

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

3

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

4

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

5

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

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?