Refactoring Framework
News
- 1st July 2009: Version 0.0.1 released. It is based on Rodin 1.0.0 RC1.
The Rename Refactoring Plug-in
User:Renato at Southampton is in charge of the Refactoring Framework.
One of the most recurring requirement from users of the Rodin platform is to have simple means for renaming modeling elements. Users want to have a unique operation that will rename an element both at its declaration and all its occurrences. Moreover, they require that renaming an element doesn't modify their existing proof state (no loss of proof).
This requirement falls in the more general context of refactoring. In software engineering, "refactoring" source code means improving it without changing its overall results, and is sometimes informally referred to as "cleaning it up". In the case of the Rodin platform, the refactoring framework is related to the first option, where refactoring should not change the overall behaviour of the files/elements, nor loosing proofs.
The following diagram shows the architecture of the refactoring framework.
The Rename Refactoring Framework Architecture
Currently, it is being developed the application of such framework to event-b files (context, machines, proofs obligations, etc) and elements (constants, variables, carrier sets, etc). There are still some tests to be run for the different elements of contexts and machines. The next goal would be to apply and use this framework on Rodin (together with file editors or perspectives).
Refactoring Trees after processing the extension points
Since there are proof obligations associated with Event-B files, while renaming the goal would be to cause the less effort as possible on re-proving and if possible re-using the proofs that are already discharged. The refactoring should not change the semantic of any of the elements/files. Instead, it should just change names or labels, so the proofs should not have to be re-generated (nor re-discharged). That is one of final goals while applying of this framework to Event-B.
Initial Work
Initial work towards implementation of this framework is described in Sonja Holl's Bachelor thesis
Installing/Updating
The installation or update for the renaming/refactoring plug-in is available under the main Rodin Update site (http://rodin-b-sharp.sourceforge.net/updates). There is a problem with the categories: the 'Renaming and Refactory' category is empty and the installation is available at 'Uncategorized' category. Should be solved soon. Like always, after the installation, restarting the application is recommended.
Usage
The Renaming/Refactory plug-in allows the renaming of:
- Variables
- Parameters
- Carrier Sets
- Constants
- Events
- Other labelled elements (invariants, axioms, guards, etc)
Requirements before using
Before using the renaming/refactory, all the files in the project should be saved ( it will be asked to save in there are any unsaved files). There should be no errors in the project, otherwise it could lead to even more errors after applying the renaming.
Steps of usage
- User selects element to be renamed at the Event-B Explorer
- By right clicking in the element, there should appear an option 'Refactory...'. Selecting that option should open a wizard
- User introduces new element name in the first page of the wizard. Then click in 'Next'.
- A list of related files is created and the plug-in check for possible clashes and returns a report
- User decides if he wants to execute renaming (by clicking in 'Finish')
Bugs, Features and Comments
Any reports of bugs, features or comments are welcome. You can add any of them here.
Bugs
- -
Features
- -
Comments
- -
Releases
Version 0.0.1
1st July 2009
A release of renaming/refactory (v0.0.1) compatible with Rodin v1.0.0 is already available in the main Rodin update site.
Note that this version is still a prototype so prone to errors. So it is suggested to back up the projects before starting to use the renaming plug-in. The plug-in uses the most recent version of Rodin Indexer. Before starting the renaming, it is recommended to clean and build the project in order to have the indexer tables updated.
Although one of the goals is to the rename the respective proof obligations, this feature is not available in this version. It should be available in the next release. If you find bugs or errors, please let me know by updating this wiki-page or email.
