A rigorous approach for proving model refactorings Gheyi, Rohit; Massoni, Tiago; Borba, Paulo
Proceedings of the 20th IEEE/ACM International Conference on Automated Software Engineering,
11/2005
Conference Proceeding
Both model and program 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. In this paper, we propose guidelines ...on how to rigorously prove model refactorings for Alloy, a formal object-oriented modeling language. We use the Prototype Verification System (PVS) to specify and prove the soundness of the transformations. Proposing refactorings in this way can facilitate not only design, but also improve the quality of refactoring tools.
Currently analysis of refactoring in software repositories is either manual or only syntactic, which is time-consuming, error-prone, and non-scalable. Such analysis is useful to understand the ...dynamics of refactoring throughout development, especially in multi-developer environments, such as open source projects. In this work, we propose a fully automatic technique to analyze refactoring frequency, granularity and scope in software repositories. It is based on SAFEREFACTOR, a tool that analyzes transformations by generating tests to detect behavioral changes - it has found a number of bugs in refactoring implementations within some IDEs, such as Eclipse and Netbeans. We use our technique to analyze five open source Java projects (JHotDraw, ArgoUML, SweetHome 3D, HSQLDB and jEdit). From more than 40,723 software versions, 39 years of software development, 80 developers and 1.5 TLOC, we have found that: 27% of changes are refactorings. Regarding the refactorings, 63,83% are Low level, and 71% have local scope. Our results indicate that refactorings are frequently applied before likely functionality changes, in order to better prepare design for accommodating additions.
A model-driven approach to formal refactoring Massoni, Tiago; Gheyi, Rohit; Borba, Paulo
Companion to the 20th annual ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications,
10/2005
Conference Proceeding
Open access
Applying refactorings to object-oriented systems usually affects source code and its associated models, involving complex maintenance efforts to keep those artifacts up to date. Most projects abandon ...design information in the form of models early in the life cycle, as their sustentation becomes extremely expensive. We propose a formal approach to consistently refactor systems in a model-driven manner. The refactoring applied to the model is linked to a sequence of behavior-preserving transformations that automatically refactor the underlying source code, based on structural properties from the model that must be implemented by the program. As a consequence, sound program refactoring can be accomplished without developer intervention, based only on the applied model transformations. Also, the refactored source code is consistent with the refactored model. Model information can be additionally used to improve refactoring automation, as more powerful transformations can be mechanized.
Object-oriented programming laws have been proposed in the context of languages that are not combined with a behavioral interface specification language (BISL). The strong dependence between ...source-code and interface specifications may cause a number of difficulties when transforming programs. In this paper we introduce a set of programming laws for object-oriented languages like Java combined with the Java Modeling Language (JML). The set of laws deals with object-oriented features taking into account their specifications. Some laws deal only with features of the specification language. These laws constitute a set of small transformations for the development of more elaborate ones like refactorings.
PDF