{"content":[{"text":"we want to assure that the semantics is preserved. However, we may also want to make \n changes in the speciﬁcations that do not preserve semantics. In these cases, the basic laws \n proposed next are not suitable but this is trivially done by the user. Furthermore, it is a \n good practice to show that the set of laws that we proposed are complete in some sense. \n The standard approach is to show that the basic set of laws is sufﬁcient to transform any \n arbitrary model into a normal form expressed in terms of a small subset of the language \n operators [Hoare et al., 1987]. This, however, is beyond the scope of this article. \n A similar work has been done for Reﬁnement Object Oriented Language (ROOL) \n [Borba and Sampaio, 2000]. However, ROOL is less powerful for specifying structural \n properties among types. Whereas ROOL supports only attribute declarations, as in Java \n [Gosling et al., 1996], Alloy supports the declaration of bidirectional relations with arbi- \n trary arities and multiplicities, as in UML with OCL. Another difference is that in ROOL \n we can not deﬁne global constraints, such as those involving cardinality (number of in- \n stances) of classes in the entire system. In Alloy and UML with OCL this is possible. \n Related approaches [Lano and Bicarregui, 1998, Gogolla and Richters, 1998, \n Suny´e et al., 2001, Evans, 1998] have proposed some transformations of UML models. \n However some of the transformations do not completely preserve semantics. Further- \n more, they are different from ours since they do not propose a small set of small-grain \n transformations. They are much similar to refactorings, which are large-grain transforma- \n tions that preserve semantics and may improve readability, design structure and reusabil- \n ity. \n Model transformations are useful because it is easier to transform models rather \n than code. Usually, we only refactor code. Nevertheless, if we build a tool to relate code \n and model transformations automatically, we only need to make changes in the models \n which are simpler, and it automatically maps changes to the code. \n The remainder of this paper is organized as follows. Section 2 overviews the \n Alloy language. In Section 3, we present some basic laws for Alloy. The following \n section illustrates how the laws presented in the previous section can be used to formally \n refactor a design model for Java types. Finally, Section 5 discusses some related work \n and presents our conclusions.","bbox":{"left":0.142992,"top":0.066569,"width":0.714055,"height":0.544832}},{"text":"2. Alloy \n Alloy is a strongly typed language that assumes a universe of elements partitioned into \n subsets, each of which is associated with a basic type. An Alloy model or speciﬁcation is a \n sequence of paragraphs of two kinds: signatures that are used for deﬁning new types, and \n formulas paragraphs, like facts and functions, used to record constraints. Each signature \n has a set of objects (elements). These objects can be related by the relations declared in \n the signatures. \n A signature paragraph introduces a basic type – if it does not extend another signa- \n ture – and a collection of relations, called ﬁelds, along with the types of the ﬁelds and other \n constraints on the values they relate. If a signature extends another, then its type is the \n parent signature type. Besides signature extension, Alloy has other important structures \n and operators like modules, polymorphism, commands for analyzing the speciﬁcation, \n that can be found elsewhere [Jackson et al., 2001]. \n Suppose that we want to model in Alloy part of a bank system where each bank \n has a set of accounts and each account has an identiﬁer that is unique. Figure 1 describes \n the object model [Liskov and Guttag, 2001] of the system. Each box in an object model \n represents a set of objects. The arrows are relations, sometimes called associations, and","bbox":{"left":0.142992,"top":0.638098,"width":0.7137739999999999,"height":0.3152029999999999}}],"images_bbox":[],"images_bbox_not_text_overlap":[]}