- ...situations.
- The weaker meaning requires each method to
preserve the invariant of the class it belongs to. Assume two
objects X and Y of classes CX and CY that reference a common
object Z of class CZ. Obviously it is possible to violate the
invariant of CY via methods of CX and CZ (which do not need
to preserve invY). Thus, we cannot make use of invY during the
verification of Y because it may not hold.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
- ...m
- We assume that invariants may only
state properties of reachable objects. An object X is reachable
from object Y if there is a chain of references from Y to
X.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
- ...module.
- Note, that a class can be semantically private despite being
syntactically public.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
- ...invariant.
- The stronger invariant requires stronger
preconditions for some methods, e.g., the multiplication
method. Thus, the new class is not a behavioral subtype of
fraction.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.