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

which each model transformation is associated with a synchronizer , a sequence
of program transformations, which (1) updates code declarations and (2) adapts
statements according to the modified declarations - as explained in Section 3.
This unidirectional (model to code) approach to synchronization presents a fun-
damental effect: it allows powerful program refactoring directly from abstract
information provided by object model invariants. Previous publications delin-
eate the model-driven approach to refactoring [14], and preliminary conclusions
on the use of invariants as basis for automatic refactoring [15]. Those contribu-
tions are extended in this paper with a description of synchronizers, soundness
proofs and discussion (Sections 3, 4 and 5, respectively).
We establish our theory on previous work in primitive model [16] and program
transformations [17,18]. Object models in Alloy [3] express objects, relations and
invariants equivalently to the core concepts of UML class diagrams. For pro-
grams, we consider a Java-like language [19]. These languages are explained in
Section 2. A general soundness theorem is defined and proved for synchronizers
(Section 4); in this proof, we ensure that synchronizers are program refinements
(preserving behavior) and the refactored program is consistent with the refac-
tored model. Consistency is defined in terms of syntax and semantics; only the
syntactic consistency must be adjusted for other languages - the semantic map-
ping is language independent. The need for the proved properties unveils issues
that will recur in several MDD contexts that employ object models, related to
automation and refactoring quality (Section 5).

2 Languages

In our theory, we consider object models in Alloy [3], and programs in a Java-like
language, developed for reasoning about object-oriented programming [19].

2.1 Model Refactoring

Alloy [3] presents formal type system and semantics for writing object models.
An Alloy model contains a sequence of paragraphs ;a signature defines a new
type. A signature paragraph introduces a basic type and a collection of rela-
tions , along with their types and constraints on their values. For instance, an
object model for a file system defines signatures for FSObject and Name - set
defines unconstrained relations. In Alloy version 3, one signature can extend an-
other, establishing that the extended signature is a subset of its supersignature
( File ). In addition, facts are used to package model invariants. In the following
fragment, the formula states that, from all file system objects, only directories
may contain other objects. The join operator '.' represents relational dereference,
and FSObject - Dir expresses all FSObjects instances that are not directories
(set difference has the conventional meaning).

sig Name {}
sig FSObject { name: set Name, contents: set FSObject }

fact { (FSObject-Dir).contents = {} }
sig File extends FSObject {}