%0 Journal Article %1 gheyi_07_static %A Gheyi, Rohit %A Massoni, Tiago %A Borba, Paulo %C Amsterdam, The Netherlands, The Netherlands %D 2007 %I Elsevier Science Publishers B. V. %J Electron. Notes Theor. Comput. Sci. %K _hardcopy 2007 semantics alloy refactoring %P 209--233 %R 10.1016/j.entcs.2007.03.023 %T A Static Semantics for Alloy and its Impact in Refactorings %U http://dx.doi.org/10.1016/j.entcs.2007.03.023 %V 184 %X Refactorings are usually proposed in an ad hoc way because it is difficult to prove that they are sound with respect to a formal semantics, not guaranteeing the absence of type errors or semantic changes. Consequently, developers using refactoring tools must rely on compilation and tests to ensure type-correctness and semantics preservation, respectively, which may not be satisfactory to critical software development. In this paper, we formalize a static semantics for Alloy, which is a formal object-oriented modeling language, and encode it in Prototype Verification System (PVS). The static semantics^a€™ formalization can be useful for specifying and proving that transformations in general (not only refactorings) do not introduce type errors, for instance, as we show here.

@article{gheyi_07_static, abstract = {Refactorings are usually proposed in an ad hoc way because it is difficult to prove that they are sound with respect to a formal semantics, not guaranteeing the absence of type errors or semantic changes. Consequently, developers using refactoring tools must rely on compilation and tests to ensure type-correctness and semantics preservation, respectively, which may not be satisfactory to critical software development. In this paper, we formalize a static semantics for Alloy, which is a formal object-oriented modeling language, and encode it in Prototype Verification System (PVS). The static semantics^{a}€™ formalization can be useful for specifying and proving that transformations in general (not only refactorings) do not introduce type errors, for instance, as we show here.}, added-at = {2009-02-11T20:50:30.000+0100}, address = {Amsterdam, The Netherlands, The Netherlands}, author = {Gheyi, Rohit and Massoni, Tiago and Borba, Paulo}, biburl = {https://www.bibsonomy.org/bibtex/2d3d89085269a01090e10bb2bc79a9051/leonardo}, citeulike-article-id = {1550798}, doi = {10.1016/j.entcs.2007.03.023}, interhash = {165052978993e9d3b5b0a59fb1bbfc46}, intrahash = {d3d89085269a01090e10bb2bc79a9051}, issn = {1571-0661}, journal = {Electron. Notes Theor. Comput. Sci.}, keywords = {_hardcopy 2007 semantics alloy refactoring}, pages = {209--233}, posted-at = {2007-08-10 03:28:24}, priority = {3}, publisher = {Elsevier Science Publishers B. V.}, timestamp = {2009-02-11T20:50:30.000+0100}, title = {A Static Semantics for Alloy and its Impact in Refactorings}, url = {http://dx.doi.org/10.1016/j.entcs.2007.03.023}, volume = 184, year = 2007 }