Synchronizing Model and Program Refactoring - Formal Methods: Foundations and Applications - page 101

Fig. 1. Model-driven refactoring with synchronizers
high-level assumptions about the program. In fact, we analyzed each Alloy law
and conceived synchronizers for both application directions.
A synchronizer must then exhibit the following characteristics: it rewrites pro-
grams for updating corresponding abstractions that were refactored in the object
model, and preserves program behavior. Therefore, every synchronizer fulfills a
few requirements: its application results in programs that refine the previous
version and establish consistency with the refactored model, syntactically and
semantically, as explained next. In addition, confinement is maintained.
3.2 Consistency Relationship
A desirable property of object models is abstraction; ideally, they can be imple-
mented by several structurally-distinct programs, as long as the invariants hold
during their executions. Structures in the model must be somehow implemented
in the program, offering a basis for evaluating whether the modeled constraints
are met. We call this correspondence syntactic consistency . Given a syntactic
consistency relationship, fulfillment of model invariants by the executions of a
given program is regarded as semantic consistency .
We chose a particular syntactic consistency: there must be one direct class
for each signature declared in the model (for simplicity, this specification relies
on the equality between names, although a mapping between names could be
easily established as well). Also, all supersignatures of a signature must have
corresponding superclasses of class S, indicating that more superclasses may
be declared in the program, but the modeled hierarchy is maintained. Likewise,
every relation is mapped to one field with an exactly matching type, with one ad-
ditional constraint: relations with single multiplicity (yielding a scalar value) are
mapped to single field, whereas relations with set multiplicity must be mapped to
collection-type fields. Additional classes, fields or methods can be freely declared
in the program.