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.
%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
}