Refactoring Framework: Difference between revisions
imported>Renato New page: User:Renato at Southampton is in charge of the Refactoring Framework. In software engineering, "refactoring" source code means improving it without changing its overall result... |
imported>Laurent Added ref to Sonja's thesis |
||
| Line 16: | Line 16: | ||
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. | 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 [http://www.stups.uni-duesseldorf.de/thesis_detail.php?id=9 Sonja Holl's Bachelor thesis] | |||
[[Category:Design]] | [[Category:Design]] | ||
Revision as of 15:33, 6 January 2009
User:Renato at Southampton is in charge of the Refactoring Framework.
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 this case, the refactoring framework is related to the first option, where refactoring should not change the overall behaviour of the files/elements.
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
