Chapter 10

Instructors' Guide

Ch 1 Ch 2 Ch 3 Ch 4 Ch 5 Ch 6 Ch 7 Ch 8 Ch 9 Ch 10 Ch 11 Ch 12
  1. Conformance not only involves syntactic properties, but behavioral properties as well. Behavioral properties include invariant properties and history properties. See slide 10-properties.
  2. See slide 10-history.
  3. Static constraints may be expressed directly in the signature, but also by means of pre- and post-conditions. To a certain, but definitely lesser, extent, the reverse is also true. See slide 10-constraints.
  4. States may be modeled as functions and state transformations as function modifications. See slide 10-verification and slide 10-subst.
  5. There are two ways to verify the behavior of a program: (a) prove for each possible transition that the formula holds; and (b) employ the correctness calculus given in slide 10-correctness.
  6. For each syntactical kind of statement allowed by the language, a transition system specifies a corresponding execution step, or series of such steps, by means of a transition derivation rule. An example transition system for a simple object-based language, supporting object creation and message passing, is given in section behavior.
  7. To prove that a realization is correct with respect to its abstract specification, one must prove that each concrete operation satisfies the constraints imposed on the abstract level. See slide 10-ADT.
  8. See slide 10-specification, slide 10-realization and slide 10-absf.
  9. Correspondence between subtypes involves syntactic constraints, defined by the subtyping rules given in chapter 9, behavioral constraints, as characterized by the refinement relation for pre- and post-conditions and invariants, and constraints for the extensions, as expressed by the diamond rule. See slide 10-correspondence and slide 10-subtyping.
  10. See slide 10-ex-subtype, slide 10-ex-correspondence and slide 10-ex-proof.
  11. Invariance properties of objects cannot completely be checked locally, within the confines of a single object. See slide 10-invariants. Checking invariants explicitly for each object, however, is likely to be too expensive.
  12. Formal methods to specify the interaction between objects include model-based specification methods, the specification of contracts as behavioral compositions, the specification of cooperating actors by means of scripts, the specification of multi-party interactions, and the specification of joint action systems. See slide 10-interaction.

slide: Answers