Article,
Alloy as a Refactoring Checker?
Electronic Notes in Theoretical Computer Science, (June 2008)
DOI: http://dx.doi.org/10.1016/j.entcs.2008.06.015
Abstract
Refactorings are systematic changes made to programs, models or specifications in order to improve their structure without changing the externally observable behaviour. We will examine how a constraint solver (the Alloy Analyzer) can be used to automatically check if refactorings, applied to a formal specification (written in Z), meet this requirement. Furthermore, we identify a class of refactorings for which the use of this tool is reasonable in general.
