A Model-driven Approach to Formal Refactoring

AUTOR(ES)
DATA DE PUBLICAÇÃO

2008

RESUMO

Refactoring object-oriented software, as any other evolutionary tasks usually affects source code and object models, burdening developers to keep those artifacts correct and up to date Due to the gap between modeling and programming artifacts, refactoring efforts soon become duplicate and considerably expensive. In this context, currently used tool support, in special Round-Trip Engineering SORTER tools, fails to fully automate evolution tasks. Consequently, most projects discard object models early in the life cycle, adhering to code-driven approaches. This thesis proposes a formal approach to consistently refactor object models and object-oriented programs of a system in a model-driven manner. Model refactoring is backed by formal laws of modeling, which are guaranteed to be semantics preserving. Each refactoring, a composition of laws, applicable to an object model, is associated with a emi-automatic sequence of applications of laws of programming, called strategy. Strategies are applied by relying on a specific conformance relationship between object models and programs, which must fulfill a pecific degree of confinement. We formalized 14 strategies, two for each law of modeling that affects program structures. These strategies have been formalized as refinement tactics. In such scenario, complex refactoring that affect main program structures can be applied abstractly, leaving the update of implementation details to strategies. Also, model invariant can be used to improve refactoring automation, as they provide runtime information that allows automation of more powerful program refactoring. This thesis considers Alloy as the formal modeling language, along with a simplified Java-like programming language that we call EN. For this programming language, we introduced four new refactoring and laws of object-oriented programming, with their correspondent derivations and proofs. Also, the laws of programming have been used in a reference semantics context, which is closer to current mainstream programming languages. In order to delimitate the applicability of model-driven refactoring, we formalize a specific conformance relationship, using a underlying general framework for formalizing conformance relationships; the related formal definitions have been specified and type-checked with PVS. In addition, we establish and manually prove a soundness theorem for trategie, guaranteeing that they preserve the target programed behavior and conformance. Despite of its formality, we also regard the utilization of this theory in practical objectoriented development, by discussion and three case studies that simulate refactoring situations for object models and programs. The results presented here shows evidence on issues that will surely recur in other Model-Driven Development contexts

ASSUNTO(S)

refatoramento connamento confinement desenvolvimento dirigido por modelos alloy ciencia da computacao alloy refactoring model-driven development

ACESSO AO ARTIGO

Documentos Relacionados