Refactoring Framework: Difference between revisions
imported>Renato |
imported>Andy |
||
| (27 intermediate revisions by 4 users not shown) | |||
| Line 4: | Line 4: | ||
==News == | ==News == | ||
* '29th June 2011'': [[#Version_1. | * ''6th May 2014'' : [[#Version_1.3.0|Version 1.3.0]] released. It is based on Rodin 3.0.x. | ||
* '8th Nov 2010'': [[#Version_1.0.0|Version 1.0.0]] released. It is based on Rodin 2.0.x. | * ''25th June 2012'' : [[#Version_1.2.2|Version 1.2.2]] released. It is based on Rodin 2.5.x. | ||
* '28th May 2010'': [[#Version_0.0.8|Version 0.0.8]] released. It is based on Rodin 1.3.x. | * ''29th June 2011'' : [[#Version_1.2.0|Version 1.2.0]] released. It is based on Rodin 2.2.x. | ||
* ''30th March 2010'': [[#Version_0.0.7|Version 0.0.7]] released. It is based on Rodin 1.2.x. | * ''8th Nov 2010'' : [[#Version_1.0.0|Version 1.0.0]] released. It is based on Rodin 2.0.x. | ||
* ''28th May 2010'' : [[#Version_0.0.8|Version 0.0.8]] released. It is based on Rodin 1.3.x. | |||
* ''30th March 2010'' : [[#Version_0.0.7|Version 0.0.7]] released. It is based on Rodin 1.2.x. | |||
* ''25th February 2010'': [[#Version_0.0.6|Version 0.0.6]] released. It is based on Rodin 1.2.x. | * ''25th February 2010'': [[#Version_0.0.6|Version 0.0.6]] released. It is based on Rodin 1.2.x. | ||
* ''13th January 2010'': [[#Version_0.0.5|Version 0.0.5]] released. It is based on Rodin 1.1.0. | * ''13th January 2010'': [[#Version_0.0.5|Version 0.0.5]] released. It is based on Rodin 1.1.0. | ||
| Line 16: | Line 18: | ||
==The Rename Refactoring Plug-in == | ==The Rename Refactoring Plug-in == | ||
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). | 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). | ||
| Line 25: | Line 25: | ||
The following diagram shows the architecture of the refactoring framework. | The following diagram shows the architecture of the refactoring framework. | ||
[[Image:Architecture_refactoring_framework.jpg]] | [[Image:Architecture_refactoring_framework.jpg|500x400px]] | ||
==The Rename Refactoring Framework Architecture == | ==The Rename Refactoring Framework Architecture == | ||
| Line 31: | Line 31: | ||
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). | 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). | ||
[[Image:RefTree. | [[Image:RefTree.jpg|center|450x400px]] | ||
==== Refactoring Trees after processing the extension points ==== | ==== Refactoring Trees after processing the extension points ==== | ||
| Line 39: | Line 39: | ||
==Initial Work == | ==Initial Work == | ||
Initial work towards implementation of this framework is described in [http:// | Initial work towards implementation of this framework is described in [http://stups.hhu.de/mediawiki/images/9/94/Holl2007_Bachelorarbeit.pdf Sonja Holl's Bachelor thesis] | ||
==Installing/Updating == | ==Installing/Updating == | ||
| Line 63: | Line 63: | ||
# User selects element to be renamed at the Event-B Explorer | # 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 [[Image:refactory menu.png]] | # By right clicking in the element, there should appear an option 'Refactory...'. Selecting that option should open a wizard [[Image:refactory menu.png|300x300px]] | ||
# User introduces new element name in the first page of the wizard. Then click in 'Next'. [[Image: | # User introduces new element name in the first page of the wizard. Then click in 'Next'. [[Image:new_name_wizard2.png|400x350px]] | ||
# If the option '''Wait for Indexer to update''' is selected, then '''if the rodin indexer is not up to date, the user has to wait for it. Otherwise, the user can cancel the operation and try later. ''' [[Image:Refactory_progress_updating_rodin_indexer.png| middle |300x300px]]. If the option '''Wait for Indexer to update''' is not selected, the tool will use the previous version of the indexer and rename accordingly. | |||
# Once the indexer is up to date, the user can proceed with the operation.[[Image:refactory_rodin_indexer_updated.png|350x300px]] | |||
# A list of related files is created and the plug-in check for possible clashes and returns a report | # 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') | # User decides if he wants to execute renaming (by clicking in 'Finish') | ||
[[Image:refactory_report_wizard.png|400x300px]] | |||
[[Image:refactory_report_wizard.png]] | |||
== Bugs, Features and Comments == | == Bugs, Features and Comments == | ||
''Any reports of bugs, features or comments are welcome. | ''Any reports of bugs, features or comments are welcome. Please, use the SourceForge trackers to report a bug on existing features, or to request new features:'' | ||
=== | * [https://sourceforge.net/tracker/?atid=651669&group_id=108850&category=1259297 Bugs] | ||
* [https://sourceforge.net/tracker/?atid=651672&group_id=108850&category=1259298 Feature Requests] | |||
====Features Request==== | ====Features Request==== | ||
* Implement UNDO for renaming | * Implement UNDO for renaming | ||
==== | == Releases == | ||
* | |||
=====Version 1.3.0 ===== | |||
''6th May 2014'' | |||
This new release is a port to Rodin 3.x. | |||
=====Version 1.2.2 ===== | |||
''25th June 2012'' | |||
A release of renaming/refactory (v1.2.2) compatible with Rodin v2.5 is available in the main Rodin update site (Utilities category). | |||
*Bug fix | |||
** Fixed bug related with waiting for the rodin indexer to update | |||
== | *Feature Request: | ||
** Added option to rename without having to wait for the rodin indexer to update. | |||
=====Version 1.2.0 ===== | |||
''29th June 2011'' | |||
A release of renaming/refactory (v1.2.0) compatible with Rodin v2.2.x is available in the main Rodin update site. | |||
*Bug fix | |||
** Before renaming, ignore unsaved files that finish with 'tmp'. | |||
** Sometimes platform would hang when renaming. This happens because the rodin indexer is still updating when the renaming operation is called and the platform would hang/block until the indexer had finished updating. To circumvent this problem, an additional wizard step is added corresponding to the indexer update. That step allows the user to stop the renaming and start later without hanging the platform. | |||
*Feature Request: | |||
** More accurate monitor progress bar. | |||
** Shorter description of reasoner version problem. | |||
**Optimised rewriting of freeIdentifiers when renaming variables and constants. | |||
=====Version 1.0.0 ===== | =====Version 1.0.0 ===== | ||
| Line 178: | Line 200: | ||
[[Category:Design]] | [[Category:Design]] | ||
[[Category:Plugin]] | |||
[[Category:User documentation]] | |||
Latest revision as of 07:41, 12 January 2016
News
- 6th May 2014 : Version 1.3.0 released. It is based on Rodin 3.0.x.
- 25th June 2012 : Version 1.2.2 released. It is based on Rodin 2.5.x.
- 29th June 2011 : Version 1.2.0 released. It is based on Rodin 2.2.x.
- 8th Nov 2010 : Version 1.0.0 released. It is based on Rodin 2.0.x.
- 28th May 2010 : Version 0.0.8 released. It is based on Rodin 1.3.x.
- 30th March 2010 : Version 0.0.7 released. It is based on Rodin 1.2.x.
- 25th February 2010: Version 0.0.6 released. It is based on Rodin 1.2.x.
- 13th January 2010: Version 0.0.5 released. It is based on Rodin 1.1.0.
- 5th November 2009: Version 0.0.4 released. It is based on Rodin 1.1.0.
- 2nd November 2009: Version 0.0.4 released. It is based on Rodin 1.1.0.
- 3rd July 2009: Version 0.0.2 released. It is based on Rodin 1.0.
- 1st July 2009: Version 0.0.1 released. It is based on Rodin 1.0.0 RC1.
The Rename Refactoring Plug-in
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) and category 'Utilities'. 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 if there are unsaved files). There should be no errors in the project, otherwise it could lead to even more errors after applying the renaming (warning).
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'.
- If the option Wait for Indexer to update is selected, then if the rodin indexer is not up to date, the user has to wait for it. Otherwise, the user can cancel the operation and try later.
. If the option Wait for Indexer to update is not selected, the tool will use the previous version of the indexer and rename accordingly. - Once the indexer is up to date, the user can proceed with the operation.
- 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. Please, use the SourceForge trackers to report a bug on existing features, or to request new features:
Features Request
- Implement UNDO for renaming
Releases
Version 1.3.0
6th May 2014
This new release is a port to Rodin 3.x.
Version 1.2.2
25th June 2012
A release of renaming/refactory (v1.2.2) compatible with Rodin v2.5 is available in the main Rodin update site (Utilities category).
- Bug fix
- Fixed bug related with waiting for the rodin indexer to update
- Feature Request:
- Added option to rename without having to wait for the rodin indexer to update.
Version 1.2.0
29th June 2011
A release of renaming/refactory (v1.2.0) compatible with Rodin v2.2.x is available in the main Rodin update site.
- Bug fix
- Before renaming, ignore unsaved files that finish with 'tmp'.
- Sometimes platform would hang when renaming. This happens because the rodin indexer is still updating when the renaming operation is called and the platform would hang/block until the indexer had finished updating. To circumvent this problem, an additional wizard step is added corresponding to the indexer update. That step allows the user to stop the renaming and start later without hanging the platform.
- Feature Request:
- More accurate monitor progress bar.
- Shorter description of reasoner version problem.
- Optimised rewriting of freeIdentifiers when renaming variables and constants.
Version 1.0.0
8th Nov 2010
A release of renaming/refactory (v1.0.0) compatible with Rodin v2.0.x is available in the main Rodin update site.
Version 0.0.8
28th May 2010
A release of renaming/refactory (v0.0.8) compatible with Rodin v1.3.x is available in the main Rodin update site. A bug related to assignment using the "become such that" operator was fixed. Also, when renaming proofs, this is done by running a job which can run in background.
- Bug Fix
- Bug 3005170: If a variable is renamed, which is used in a "becomes such that", the assignment does not type check any longer after the renaming operation, because the variable has disappeared.
- Bug 3005202: When a renaming operation is performed, the provers are launched. The waiting time may be quite long and it is impossible to do anything else.
It is always necessary to run the provers? If it is indeed mandatory, the provers should be temporarily disconnected until the renaming has been performed, and run when this operation has completed.
Version 0.0.7
30th March 2010
A release of renaming/refactory (v0.0.7) compatible with Rodin v1.2.x is available in the main Rodin update site.
- Bug Fix
- Fix bug that occurred when renaming an event whose machine was refined.
Version 0.0.6
25th February 2010
A release of renaming/refactory (v0.0.6) compatible with Rodin v1.2.x is available in the main Rodin update site.
- Feature Request
- Renaming of all proofs after the element renaming. For each proof obligation, if proof rebuilding does not work, a new proofTree is created based on the initial proofTree and on the renamed element. By applying the ancient rule, if a proof is discharged before the renamed, it remains discharged after the renaming.
Version 0.0.5
13th January 2010
A release of renaming/refactory (v0.0.5) fixing a few bugs found is already available.
Version 0.0.4
5th November 2009
A release of renaming/refactory (v0.0.4) compatible with Rodin v1.1.0 is available in the main Rodin update site (bug fix from 0.0.3). Before starting the renaming, it is recommended to clean and build the project in order to have the indexer tables updated (IMPORTANT).
- Bug fix
- Renaming of proofs would not save the proof files after renaming
- Renaming of labelled elements would not update the proofs.
- Possible Problem
- If you try to rename and the operation runs successfully without any errors but does not have any effect, you should:
- First, try to fix the renaming manually on the respective file (or using the renaming framework, revert to the original name)
- Try to make a CLEAN and BUILD to ensure that the Rodin indexer is updated before the renaming.
- Run the renaming again and should be working fine.
- If you try to rename and the operation runs successfully without any errors but does not have any effect, you should:
Version 0.0.3
2nd November 2009
A release of renaming/refactory (v0.0.3) compatible with Rodin v1.1.0 is already available in the main Rodin update site. Before starting the renaming, it is recommended to clean and build the project in order to have the indexer tables updated.
- Features
- Renaming of machines and contexts is possible using the indexers. After the renaming of a machine/context, the change is propagated over the related files
- Renaming of proofs: after the renaming, the proof obligations are also updated to reflect the renaming. It might be necessary to manually refresh the status of some proof obligations (although the proof is already discharged). This renaming is not fully-functional at the moment and some discharged proof obligations may have to be discharged again. We intend to fix this problem in the future.
Version 0.0.2
3rd July 2009
- Bugs
- Validate if new name is in the list of reserved words of Event-B (dom,ran, card, etc)
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.
