PhD thesis,
A Refinement Theory for Alloy
Universidade Federal de Pernambuco, (July 2007)
Abstract
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 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 have operations or 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 propose a set of semantics-preserving structural model transformations for Alloy, which is a formal object-oriented modeling language. We specify in PVS well-formedness rules and extend the semantics proposed for Alloy, 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 show that it is compositional and relate it to the data refinement notion for Z. 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.
