Hi Bryan:
do you agree with those definitions and the theorem?
Can you prove the theorem?
Definition:
For a class graph G a transform X->Y is valid if for all og in Objects(G)
and all replacements of an X-object in og
by a Y-object we obtain an object in Objects(G).
For definition of Objects(G): paper with Mitch Wand.
Theorem:
For a class graph G a transform X->Y is valid
if for all construction edges -> *,*,S for some
class S that is a superclass of X, Y is a subclass of S.
Definition:
For a class graph G a transform X->Y is type correct if it is valid.
We write A <= B if A is a subclass of B. <= is a reflexive
and transitive relation. <= is the reflexive, transitive
closure defined by the ":" relation:
S: T_1 | ... | T_n
defines T_i <= S.
Implementation:
Identify all uses of a superclass of X on the right-hand-side
of a construction edge of G. For each such superclass S, check
that Y is a subclass of S.