Difference between pages "New Tactic Providers" and "Refactoring Framework"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Laurent
(→‎API Proposal: changed use of UserSupport.)
 
imported>Renato
 
Line 1: Line 1:
The purpose is to give more flexibility to tactic providers by allowing them to provide as many tactic applications as they will for a given proof node, even they apply to the same predicate and at the same position.
+
{| align="right"
 +
| __TOC__
 +
|}
  
== API Proposal ==
+
==News ==
 +
* ''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.
 +
* ''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.
  
The current proposal consists in the following published interfaces:
+
==The Rename Refactoring Plug-in ==
  
public interface ITacticProvider2 {
+
[[User:Renato]] at [[Southampton]] is in charge of the [[Refactoring Framework]].
    List<ITacticApplication> getPossibleApplications(IProofTreeNode node,
 
                                                    Predicate hyp,
 
                                                    String globalInput);
 
}
 
  
  public interface ITacticApplication {
+
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).
    ITactic getTactic(String[] inputs,
 
              String globalInput,
 
              IProgressMonitor monitor);
 
}
 
  
public interface IPositionApplication  extends ITacticApplication {
+
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.
    Point getHyperlinkBounds();
 
    String getHyperlinkLabel();
 
}
 
  
public interface IPredicateApplication extends ITacticApplication {
+
The following diagram shows the architecture of the refactoring framework.
    Image getIcon();
 
    String getTooltip();
 
}
 
  
The current extension point "proofTactics" remains unchanged.
+
[[Image:Architecture_refactoring_framework.jpg]]
  
All those interfaces are intended to be implemented by clients.
+
==The Rename Refactoring Framework Architecture ==
  
== Explanations ==
+
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).
  
The idea is to encapsulate in {{class|ITacticApplication}} all data needed by the UI to display and apply tactics.
+
[[Image:RefTree.jpg‎]]
Thus, an {{class|ITacticProvider2}}, instead of returning just one fixed tactic to apply, can return several possible 'autonomous' tactic applications.
 
  
 +
==== Refactoring Trees after processing the extension points ====
  
Interfaces {{class|IPositionApplication}} and {{class|IPredicateApplication}} are particular application types:
+
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.
  
* {{class|IPositionApplication}} is for tactics applied at a given position in a formula (red hyperlinks in interactive prover UI). The methods allow to override extension point data, in order to have a different text for each application in the hyperlink list. If '''null''' is returned, then default data from extension point is taken.
+
==Initial Work ==
  
* {{class|IPredicateApplication}} is for tactics applied at a whole predicate, like 'Contradict Goal' or 'Contradict Hyp' (icons on the left of a predicate in interactive prover UI). The methods allow to override extension point data, in order to have a different icon and tooltip for each application in the left icon list. If '''null''' is returned, then default data from extension point is taken.
+
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]
  
== Example ==
+
==Installing/Updating ==
  
The following example demonstrates (part of) the implementation of a tactic using the proposed API.
+
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.
For simplicity, a simple {{class|ITacticApplication}} is used, but a {{class|IPositionApplication}} could (should) be used instead.
 
The underlying {{class|IReasoner}} ({{class|ExampleReasoner}}) is not shown here, as it is not impacted by the proposed API.
 
  
<pre>
+
==Usage ==
// rewrites occurrences of literal 4 into either 2+2 or 2*2
 
public class ExampleTacticProvider2 implements ITacticProvider2 {
 
  
    // our own implementation of a tactic application
+
The Renaming/Refactory plug-in allows the renaming of:
    private static class ExampleApplication implements ITacticApplication {
 
  
        private final IUserSupport userSupport;
+
* Variables
        private final Predicate hyp;
+
* Parameters
        private final IPosition position;
+
* Carrier Sets
        // 2 Kinds: PLUS (2+2) and MULT (2*2)
+
* Constants
        private final ExampleReasoner.Kind kind;
+
* Events
 +
* Other labelled elements (invariants, axioms, guards, etc)
  
        public ExampleApplication(IUserSupport userSupport, Predicate hyp, IPosition position, Kind kind) {
+
====Requirements before using ====
            this.userSupport = userSupport;
 
            this.hyp = hyp;
 
            this.position = position;
 
            this.kind = kind;
 
        }
 
  
        public void apply(String[] inputs, String globalInput, IProgressMonitor monitor) {
+
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.
            try {
 
                // ExampleReasoner implements IReasoner and rewrites literal 4
 
                // at given position into:
 
                // . 2+2 if input.kind is PLUS
 
                // . 2*2 if input.kind is MULT
 
                userSupport.applyTactic(BasicTactics.reasonerTac(
 
                        new ExampleReasoner(),
 
                        new ExampleReasoner.Input(hyp, position, kind)),
 
                        true, monitor);
 
            } catch (RodinDBException e) {
 
                // log the problem
 
            }
 
        }
 
    }
 
  
    // visits a formula and adds applications on occurrences of literal 4
+
==== Steps of usage ====
    private static class ExampleApplicationVisitor extends DefaultVisitor {
 
  
        private final IUserSupport userSupport;
+
# User selects element to be renamed at the Event-B Explorer
        private final Predicate hyp;
+
# By right clicking in the element, there should appear an option 'Refactory...'. Selecting that option should open a wizard [[Image:refactory menu.png]]
        private final Predicate predicate;
+
# User introduces new element name in the first page of the wizard. Then click in 'Next'. [[Image:new_name_wizard.png]]
        // a list to put applications into
+
# A list of related files is created and the plug-in check for possible clashes and returns a report
        private final List<ITacticApplication> applications;
+
# User decides if he wants to execute renaming (by clicking in 'Finish')
  
        public ExampleApplicationVisitor(IUserSupport userSupport,
 
                Predicate predicate, Predicate hyp,
 
                List<ITacticApplication> applications) {
 
            this.userSupport = userSupport;
 
            this.predicate = predicate;
 
            this.hyp = hyp;
 
            this.applications = applications;
 
        }
 
  
        @Override
+
 
         public boolean visitINTLIT(IntegerLiteral lit) {
+
          
            if (lit.getValue().intValue() == 4) {
+
[[Image:refactory_report_wizard.png]]
                final IPosition position = predicate.getPosition(lit.getSourceLocation());
 
                applications.add(new ExampleApplication(userSupport, hyp, position, Kind.MULT));
 
                applications.add(new ExampleApplication(userSupport, hyp, position, Kind.PLUS));
 
            }
 
            return true;
 
        }
 
    }
 
  
    // the ITacticProvider2 interface method: calls the visitor on the predicate
 
    public List<ITacticApplication> getPossibleApplications(IUserSupport userSupport,
 
                                                            IProofTreeNode node,
 
                                                            Predicate hyp,
 
                                                            String globalInput) {
 
  
        final Predicate pred = (hyp == null) ? node.getSequent().goal() : hyp;
+
== Bugs, Features and Comments ==  
  
        final List<ITacticApplication> applications = new ArrayList<ITacticApplication>();
+
''Any reports of bugs, features or comments are welcome. You can add any of them here.''
       
+
 
        pred.accept(new ExampleApplicationVisitor(userSupport, pred, hyp, applications));
+
====Bugs ====
       
+
* Renaming does not work when renamed element is in variant (fixed in v0.0.5)
        return applications;
+
* Renaming proofs did not propagate over related files (fixed in v0.0.5)
    }
+
 
}
+
====Features Request====
</pre>
+
* Implement UNDO for renaming
 +
 
 +
====Comments ====
 +
* Renaming proofs ensures that all the discharged proof obligations remain discharged after the renaming (fixed in v0.0.6)
 +
 
 +
== Releases ==
 +
 
 +
=====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.
 +
 
 +
Features
 +
 
 +
Renaming of all proofs after the element renaming. If rebuilding a proof 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.
 +
 
 +
=====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]]

Revision as of 18:39, 2 March 2010

News

  • 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

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.

Architecture refactoring framework.jpg

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

RefTree.jpg

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

  1. User selects element to be renamed at the Event-B Explorer
  2. By right clicking in the element, there should appear an option 'Refactory...'. Selecting that option should open a wizard Refactory menu.png
  3. User introduces new element name in the first page of the wizard. Then click in 'Next'. New name wizard.png
  4. A list of related files is created and the plug-in check for possible clashes and returns a report
  5. User decides if he wants to execute renaming (by clicking in 'Finish')



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

  • Renaming does not work when renamed element is in variant (fixed in v0.0.5)
  • Renaming proofs did not propagate over related files (fixed in v0.0.5)

Features Request

  • Implement UNDO for renaming

Comments

  • Renaming proofs ensures that all the discharged proof obligations remain discharged after the renaming (fixed in v0.0.6)

Releases

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.

Features

Renaming of all proofs after the element renaming. If rebuilding a proof 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.
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.