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

analyzed in depth, showing issues that will recur in several MDD contexts. Thus,
proofs for synchronizers constitutes the core of our approach. Sound synchroniz-
ers depend on the defined consistency relationship and two additional properties:
(1) they must express refinements and (2) preserve program confinement.
Theorem 1 is defined for an arbitrary object model ( OM ), and an arbitrary
program ( P ), in which the application of a law to OM results in OM ,anda
synchronizer applied to P results in P . We define additional predicates from law
definitions: Refines(P',P) , in which the second argument refines the first, and
Confined(P) , stating that P satisfies the static analysis confinement rules from
Section 2.2, for a subset Own of the class table. premises ( OM, OM ,P ) states
the conditions before the application of a synchronizer, as defined in our technical
report [22] - an Alloy law applied to OM results in OM', and consistency and
confinement constraints apply to OM and P.
Theorem 1.

∀ OM, OM ,P,P • premises ( OM, OM ,P ) ⇒

syntConsistency ( OM ,P ) ∧ Confined ( P ) ∧

Refines ( P ,P ) ∧ semanticConsistency ( OM ,P )

The proof of each synchronizer is split in four supporting lemmas .Thetheorem's
meta-variables OM , OM , P and P are concretized for each synchronizer.

Lemma 1. ∀OM, OM ,P,P • premises ( OM, OM ,P ) ⇒ syntConsistency ( OM ,P )

Lemma 2. ∀OM, OM ,P,P • premises ( OM, OM ,P ) ⇒ Confined ( P )

Lemma 3. ∀OM, OM ,P,P • premises ( OM, OM ,P ) ⇒ Refines ( P ,P )

Lemma 4. ∀OM, OM ,P,P • premises ( OM, OM ,P ) ⇒ semanticConsistency ( OM ,P )

We proved the synchronizers listed in Table 1, as detailed in [17]; for illustration,
here we present the proof for removeSubclass . Model and program definitions
for the proof are shown in our technical report [22]. Assuming premises ( OM,
OM ,P ), we now prove the four previous lemmas.
Proof for Lemma 1. Since no relations are added or removed, the mapping
between relations and fields is unchanged. Regarding signatures, X is removed,
which is the only class that is removed from the program, establishing the con-
formance. The hierarchy remains unchanged. Thus syntConsistency ( OM ,P )
follows from the premises.
Proof for Lemma 2. By case analysis on P for the six static analysis rules of
confinement from Section 2.2. For each rule, we justify its maintenance in terms
of the premises and P .Inthiscase, X ∈ Rep .

1. Class B is the only one to receive new methods. If B ∈ Own ,thenfrom
premise ( OM, OM ,P ) methods previously in X could never have Rep return
types;
2. No inherited methods are added, thus from premise ( OM, OM ,P )noin-
herited methods have Rep parameters;
3. Same as above, thus from premise ( OM, OM ,P ), Rep classes do not inherit
methods from non- Rep classes;
4. No public fields of Own classes are used outside their declaring module, thus
from premise ( OM, OM ,P )no e.f is seen, unless e is self ;