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

class X extends B { constr { ..; self .type:= "X" }}

class Z extends X { constr { ..; self .type:= "Z" }}

4. Within overriding isX implementations, expression self is X is replaced
with the equivalent expression self .type = "X" ;

Regarding constructors, X declares a constructor that must be replaced, as ev-
ery new X will be rewritten as new B . Hereafter, we consider a command of
type x:= new X to be a syntactic sugar for the following sequential composi-
tion: x:= new ' X; x.newX() ,inwhich new ' is the regular instantiation of
an object, whose reference is assigned to x . It is followed by a call to newX ,a
method of class X containing the actual constructor body, used for initializing
fields. After defining this replacement for every X instantiation, the synchronizer
moves newX to the superclass B (which contains the initialization for the type
field). After this, the new 'X commands can be replaced by new 'B commands
in the whole program, with Law A. An excerpt of the result can be seen next.

class B {

.. string type ; . .

bool isX() { result := self .type= "X" ∨ self is Z }

unit newX( ) { { .. self .type:= "X" }} }
class X extends B {} ..
Bx:= new 'B;x.newX(); ..

Finally, the extends clause of X 's subclasses, then X can be eliminated. In gen-
eral, automated refactorings only remove subclasses when they are not used any-
where in the program. In contrast, this synchronizer can prepare programs when
removal of the given subclass is desirable. It replaces all uses of this subclass by
the correspondents given by an invariant (stating that class U is abstract).
The defined synchronizers follow the correspondence in Table 1. Other laws of
modeling do not have corresponding synchronizers, as they deal with syntactic
sugar in the model, which does not affect the syntactic consistency.

Table 1. Synchronizers corresponding to Alloy laws

Alloy Law synchronizer → synchronizer ←

1.Introduce Relation introduceField removeField

2.Introduce Subsignature introduceSubclass removeSubclass

3.Introduce Signature introduceClass removeClass

4.Introduce Generalization introduceSuperclass removeSuperclass

5.Split Relation splitField removeIndirectReference

6.Remove Lone Relation fromOptionalToSetField fromSetToOptionalField

7.Remove One Relation fromSingleToSetField fromSetToSingleField

4 Soundness

A soundness theorem is established for synchronizers. The rationale behind this
theorem is the set of conditions for a sound synchronized refactoring. Given these
conditions, the compromises for automating the involved transformations can be