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

5. From premise, if x:= new X was outside Own classes, X ∈ Rep .Assuming
the command is outside Own , it is impossible to have X ∈ Rep and B ∈ Rep ,

since all subclasses of Rep classes are also included. Therefore, property is
maintained;
6. From premise, e.m(..) within Own or Rep does not have Rep parameters;
no changes in parameters or Rep are made, so property is maintained.

Proof for Lemma 3. Since the synchronizer steps are exclusively defined as law
applications and class refinement [18], P refines P . Some of the applied laws
can be seen in [22] 1 .
Proof for Lemma 4. First, any interpretation can be reduced without the map-
pings to X . This is possible since values of X cannot be interpreted alone, from
the given invariant X = U − S − T . Consequently, semantics of OM is the set
of interpretations from the semantics of OM , with mapping from X removed.
Likewise, for P and P , the valid heaps of P are the valid heaps of P reduced in
mappings from the X class; this conclusion is implied from the invariant that is
assumed in the program . Also, the changed commands (type casts and tests) do
not add or remove new possible heaps; all X instances that are not B instances
are still mapped by U in the heap.

5 Discussion

In this section, the contributions and limitations of our synchronization model
are discussed, especially topics related to automation and quality of refactorings.

5.1 Invariants as Basis for Refactoring Automation

The practice of refactoring has been improved by supporting tools, avoiding
manual work and increasing trust on semantics preservation. Usually a catalog
of refactorings is offered, from which developers can choose the desired transfor-
mation for the problem in context. These automated refactorings present pre-
conditions that are checked against the code subject to refactoring, in order to
ensure correctness. While being effective to ensure safe refactorings - at least in
theory - it leads to prevention of refactoring on programs that would be eligible
if some semantic assumptions about the program behavior were considered.
Semantic assumptions about the program can be provided by object models,
then synchronizers exploit invariants to increase the applicability of some au-
tomated refactorings. Transformations based on these invariants can be applied
to programs that would not be eligible for refactoring using the current tools.
When removing a subclass, for example, the synchronizer assumes the invariant
X = U −S−T as true in every reachable program state outside a unpack/pack

1 The laws have been proven semantics preserving for a programming language without
references [18]. However, we have proven that these laws are still correct in the
presence of confinement [17].