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

Regarding model transformations in Alloy, a catalog of primitive transforma-
tions was proposed [16]. Algebraic laws formalize two primitive transformations;
equivalence allows application of the law in both directions. As an example of a
law, a new subsignature can be introduced or removed from an existing hierarchy
(Law 1). An empty subsignature X can be introduced if declared with a fresh
name. After this transformation, the supersignature U becomes abstract (defin-
ing no direct instances), as denoted by the invariant denoting the objects in X
are the objects in U , except those in S or T ( X = U−S−T ). Similarly, X can be
removed if it is not being used and no expression exp of its type exists ( exp ≤ U ,
but exp ≤ S and exp ≤ T ), where denotes subtyping. Some meta-variables

are useful as notation: rs represents relations, while forms represents a set of
formulas. Each box represents a template with which actual Alloy declarations
can match ( ps denotes the paragraphs that are not showed in the template). Ad-
ditionally, below the templates, provisos that ensure transformation correctness
are established. (

≤

← ) defines provisos for application from Left-to-Right (L-R),

while ( → ) defines provisos for applying the law from Right-to-Left (R-L).

Alloy Law 1 introduce subsignature

ps
sig U {rsU }
sig S extends U{ rsS }
sig

ps
sig U { rsU }

sig S extends U{ rsS }

U{ rsT }
sig X extends U{}
fact

T extends

sig T extends U{ rsT }

=

fact F {forms}

F {
forms
X

= U − S − T

}

provided
( → )(1) ps does not declare any paragraph named X ; (2) there is no signature in ps that extends
U ;
( ← ) X does not appear in ps , rsU , rsS , rsT and forms ; (2) there is no expression exp ,where
exp ≤ U and exp ≤ S and exp ≤ T ,in ps or forms .

The equivalence respects the notion proposed for Alloy [20]. The catalog of Alloy
laws has been proven sound and complete in a theorem prover [21]. Furthermore,
these laws can be used as basis for several applications that require semantics-
preserving transformations, such as model refactorings . Since primitive laws are
simpler - dealing with a few language constructs - they can be more easily
proven sound. By construction, a composition of laws is also correct, providing
safe refactorings for object models.

2.2 Program Refactoring

The Java-like language is inspired by Banerjee and Naumann's work [19]; it does
not consider interfaces, multithreading or library classes. A program is a set of
classes, a class table CT , which always includes a class named Main , with a main
method as the starting point of execution. A generic class declaration is defined