Instructors' Guide

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.