topical media & game development
[] readme course(s) preface I 1 2 II 3 4 III 5 6 7 IV 8 9 10 V 11 12 afterthought(s) appendix reference(s) example(s) resource(s) _

talk show tell print

object-oriented programming

[] readme course preface 1 2 3 4 5 6 7 8 9 10 11 12 appendix lectures resources

Summary

object-oriented programming

[] readme course preface 1 2 3 4 5 6 7 8 9 10 11 12 appendix lectures resources
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

1


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

2


  • 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

3


  • 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

4


  • 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

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.

object-oriented programming

[] readme course preface 1 2 3 4 5 6 7 8 9 10 11 12 appendix lectures resources

Questions

  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?
slide: Questions

object-oriented programming

[] readme course preface 1 2 3 4 5 6 7 8 9 10 11 12 appendix lectures resources

Further reading

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(s) preface I 1 2 II 3 4 III 5 6 7 IV 8 9 10 V 11 12 afterthought(s) appendix reference(s) example(s) resource(s) _

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