Difference between pages "Records Extension" and "Refactoring Framework"

Revision as of 10:47, 10 November 2009

News

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

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). 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 Request

- Implemented UNDO for renaming

Comments

-

Releases

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.

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.

@@ Line 1: / Line 1: @@
-This page is under development.
+{| align="right"
+| __TOC__
+|}
-It is intended to be a user oriented manual for using records in Event-B. This page is derived from the  [[Structured_Types|Structured Types]] page which gives a more theoretical description of the origin of the Records extension.
+==News ==
+* ''5th November 2009'': [[#Version_0.0.4|Version 0.0.4]] released. It is based on Rodin 1.1.0.
+* ''2nd November 2009'': [[#Version_0.0.4|Version 0.0.4]] released. It is based on Rodin 1.1.0.
+* ''3rd July 2009'': [[#Version_0.0.2|Version 0.0.2]] released. It is based on Rodin 1.0.
+* ''1st July 2009'': [[#Version_0.0.1|Version 0.0.1]] released. It is based on Rodin 1.0.0 RC1.
-==Introduction==
+==The Rename Refactoring Plug-in ==
-The Event-B mathematical language currently does not support a syntax for the direct definition of structured types such as records or class structures.
-The Records Extension introduces a new modelling construct to provide a notion of structured types in Event-B Contexts.
-Currently, structured variables are not supported. Variables that are typed as an instance of a record type can be thought of as identifying a particular record value. Hence it is not possible to vary an individual field, the variable must be assigned a complete new record value instance. To vary an individual field this new record value instance can be selected to have the same field value for every other field.)
+[[User:Renato]] at [[Southampton]] is in charge of the [[Refactoring Framework]].
-==UI Extensions==
+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).
-The '''Event-B editor''' is extended to include two new top level clauses. These are '''Record Declarations''' and '''Record Extensions'''.
-Records (or sub-records) are introduced in the Record Declarations clause. Records that are introduced here without a '''Supertypes''' clause are equivalent to carrier sets. Those that have a Supertypes clause are equivalent to constants that are a subset of the referenced (i.e. subtyped) record.
+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.
-Record Extensions may only add new fields to a record that has previously been declared in a Record Declaration. The extended record is referenced in an 'extends' clause.
+The following diagram shows the architecture of the refactoring framework.
-The '''Event-B navigator''' is extended to show a new node '''Records'''. Under this node are listed the records and records extensions in the Context.
+[[Image:Architecture_refactoring_framework.jpg]]
-Record Extensions are displayed as the name of the extended record appended with a + sign. Each record or record extension can be expanded to show the owned fields. (Note that this list is not cumulative, only the new fields are shown).
-(Currently in the Navigator, the Records node is shown as the first item in the Context whereas eleswhere it appears between carrier sets and constants. This is due to a limitation in the Rodin tool extension facilities).
-The '''Outline''' panel shows the records followed by record extensions as a plain list without the Records node. Again, the record or record extension can be expanded to show the fields.
+==The Rename Refactoring Framework Architecture ==
-In all  cases, the '''icon''' used for a record reflects its equivalence. That is, if it does not have a supertypes clause, it is displayed with the same icon as a carrier set. otherwise it is displayed with the same icon as a constant.
+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).
-==Semantics of Records==
+[[Image:RefTree.jpg‎]]
-The semantics of Records are given by their translation into 'pure' Event-B. This translation is performed by extensions to the static checker which generates a 'checked context' (.BCC file) containing pure Event-B from an unchecked (.BUC file) containing record elements. Hence the translated Event-B is not visible to the user.
-<formatting/presentation of this will be improved>
+==== Refactoring Trees after processing the extension points ====
-Record R Supertypes <null> --> Carrier Set R
+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.
-Record S Supertypes R          -->  Constant S,   Axiom S : POW(R)
+==Initial Work ==
-Field f : F                                -->  Constant f, Axiom f : R  --> F
+Initial work towards implementation of this framework is described in [http://www.stups.uni-duesseldorf.de/thesis_detail.php?id=9 Sonja Holl's Bachelor thesis]
-[It may be instructive to open the *.bcc file with a text editor to examine the generated carrier sets, constants, and axioms]
+==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). Like always, after the installation, restarting the application is recommended.
-==Usage==
+==Usage ==
-First define Records in the Record Declarations section. Some of these can subtype others but you need at least one that is not a subset, i.e. has no supertypes. Note that we decided not to allow records to subtype or extend Carrier Sets, but you can do the equivalent by defining a record without any fields and subtyping/extending that. Add fields and give them a type by entering an expression that evaluates to a set. (You can use records, fields, constants and sets  in the expression).
+The Renaming/Refactory plug-in allows the renaming of:
-For Record Extensions just select the record you want to add new fields to from the drop down list. and then add the new fields.
+* Variables
+* Parameters
+* Carrier Sets
+* Constants
+* Events
+* Other labelled elements (invariants, axioms, guards, etc)
-You can refer to records and fields in axioms/theorems. E.g., you could define a constant to be an instance of a record. In all cases you can refer to records and fields in the current or visible abstract (extended*) contexts.
+====Requirements before using ====
-You use fields as if they were functions (which is what they are in the checked context).
+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.
-e,g if r1, belongs to myRecord which has a field myField : NAT then I could write in a predicate... myField(r1) > 5
-==Current Limitations==
+==== Steps of usage ====
-* Records are not supported by the Camille text editor (see warning below)
-* Records are not supported by the Pretty print facility
-* Records are not supported by the Synthesis view facility
-* Records are not supported by the EventB2Latex plug-in
-* Records may have, at most, one supertype.
-* Records may only have records as supertypes (not carrier sets)
-==Warning==
+# 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]]
+# User introduces new element name in the first page of the wizard. Then click in 'Next'. [[Image:new_name_wizard.png]]
+# 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')
-Records are not supported in the Camille text editor. Editing a context that contains records with the Camille editor may result in the Records being lost.
-[[Category:Work in progress]] [[Category:Design]]
+[[Image:refactory_report_wizard.png]]
+== Bugs, Features and Comments ==
+''Any reports of bugs, features or comments are welcome. You can add any of them here.''
+====Bugs ====
+* -
+====Features Request====
+* - Implemented UNDO for renaming
+====Comments ====
+* -
+== Releases ==
+=====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.
+=====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 [mailto:ras07r@ecs.soton.ac.uk email].
+[[Category:Design]]