Rohit Gheyi

Refactorings are usually proposed in an ad hoc way because it is hard to guarantee their soundness with respect to a formal semantics. In practice, even developers using refactoring tools must have to rely on compilation and tests to guarantee semantics preservation, which may not be satisfactory to critical software development. In case of object model refactorings, most proposed transformations rely on informal argumentation. An additional problem is that equivalence notions for object models are usually too concrete in the sense that they assume that the compared models are formed of elements with the same names or structures. This is not adequate in several situations: during model refactoring, when using auxiliary model elements, or when the compared models comprise distinct but corresponding elements. In this work, we aim at proposing a set of semantics-preserving structural model transformations for Alloy, which is a formal object-oriented modeling language. We specify well-formedness rules and extend the semantics proposed for Alloy in PVS and show that these transformations are sound in the PVS theorem prover. This set of transformations is proved relatively complete in the sense that, from it, we can derive a representative set of model transformations. Moreover, we propose an abstract and flexible refinement notion for object models. Our semantics-preserving transformations are based on that. We encoded this notion in PVS and proved some properties of it. Additionally, we relate it to the traditional data refinement notion and show that it is compositional. Such semantics-preserving transformations can be applied for deriving object model refactorings and optimizing analysis. Additionally, we show how our transformations can be used to derive refactorings that formally introduce design patterns in Alloy. The proposition of a complete set of sound semantics-preserving model transformations not only contributes to the correctness to design tasks, but also improves refactoring tools.

Tiago Massoni

Refactoring object-oriented software, as any other evolutionary task, usually affects source code and related 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. Consequently, most projects discard modeling artifacts early in the life cycle, adhering to code-driven approaches. This thesis proposes a formal approach to consistently refactor systems in a modeldriven manner. Model refactoring is backed by formal primitive transformations. Each refactoring applied to a structural model is associated with a strategy of formal behaviorpreserving program transformations; structural model invariants are employed by the strategy to automatically refactor the implementation analogously. Therefore, sound program refactoring can be accomplished without developer intervention, based only on the applied model transformations. In such scenario, complex refactorings that affect main program structures can be applied abstractly, leaving the update of implementation details to the automatic strategies. Also, model invariants can be used to improve refactoring automation, as they provide runtime information that allows mechanization of more powerful program refactorings. In order to delimitate the applicability of modeldriven refactorings, we formalize a notion of conformance between structural models and programs. In addition, we establish a correctness theorem for each strategy, sketching its proof. Despite of its formality, we also regard the utilization of this theory in practical object-oriented development, by discussion and case studies.

Back