Extending the Proof Manager: Difference between revisions

From Event-B
Jump to navigationJump to search
← Older edit
imported>Son
No edit summary
imported>Ladenberger
No edit summary
 
(17 intermediate revisions by 3 users not shown)
Line 1: Line 1:
{{TOCright}}
The [[Proof Manager]] is responsible for constructing proofs and maintaining existing proofs associated with proof obligations.
The [[Proof Manager]] is responsible for constructing proofs and maintaining existing proofs associated with proof obligations.


There are two ways for extending the Proof Manager:  
There are two ways for extending the Proof Manager:  


# adding a new [[Reasoners|reasoner]].
# adding a new [http://handbook.cobra.cs.uni-duesseldorf.de/current/html/reasoners.html reasoner].


# adding a new [[Tactics|tactic]].
# adding a new [http://handbook.cobra.cs.uni-duesseldorf.de/current/html/proof_tactics.html tactic].


== Adding a New Reasoner ==
== Adding a New Reasoner ==


A reasoner is added into the Proof Manager using the extension point ''org.eventb.core.seqprover.reasoners''. Below are an example of how to contribute to the extension point.
A reasoner is added into the Proof Manager using the extension point ''org.eventb.core.seqprover.reasoners''. Below is an example of how to contribute to the extension point.


  <extension point="org.eventb.core.seqprover.reasoners">
  <extension point="org.eventb.core.seqprover.reasoners">
Line 26: Line 27:
However, most of the time, the developers only need to sub-class one of the abstract implementation, depending on the type of the reasoner. For the implementation purpose, we categorize our reasoners into the following types.  
However, most of the time, the developers only need to sub-class one of the abstract implementation, depending on the type of the reasoner. For the implementation purpose, we categorize our reasoners into the following types.  


* [[Extending the Proof Manager#Automatic Rewrite Reasoners|Automatic rewrite]] Reasoners of this type apply some rewriting rules automatically to simplify the input sequent.
* [[Adding Automatic Rewrite Reasoners | Automatic rewrite]] Reasoners of this type apply some rewriting rules automatically to simplify the input sequent.


* [[Extending the Proof Manager#Automatic Inference Reasoners|Automatic inference]] Reasoners of this type apply an inference rule automatically.
* [[Adding Manual Rewrite Reasoners | Manual rewrite]] Reasoners of this type apply a rewriting rule for a given formula (or sub-formula) in the goal or in one of the hypotheses.


* [[Extending the Proof Manager#Manual Rewrite Reasoners|Manual rewrite]] Reasoner of this type apply a rewriting rule for a given formula (or sub-formula) in the goal or in one of the hypotheses.
* [[Adding Automatic Inference Reasoners | Automatic inference]] Reasoners of this type apply an inference rule automatically.


* [[Extending the Proof Manager#Manual Inference Reasoners|Manual inference]] Reasoner of this type apply and inference rule manually.
* [[Adding Manual Inference Reasoners | Manual inference]] Reasoner of this type apply an inference rule manually.


* [[Extending the Proof Manager#General Purpose Reasoners|General purpose]] Reasoners that do not fall into the four previous categories.
* [[Adding General Purpose Reasoners |General purpose]] Reasoners that do not fall into the four previous categories.


=== Automatic Rewrite Reasoners ===
''Please also have a look at'' [[How_To_Evolve_Reasoners| How To Evolve Reasoners]].
Beside the input sequent, reasoners of this type does not have any extra input and automatically rewrites all the occurrences of certain formulas. An example of this is the rewriter which rewrites according to the following rules:


<math>
== Adding a New Tactic ==
  \begin{array}{rcl}
Adding a reasoner is only a first step in extending the Proof Manager. Reasoners need to be wrapped by Tactics for the Proof Manager to use. Similar to reasoners, there are different types of tactics for implementation purpose.
    \top \limp P & \Rightarrow & P \\
    P \limp \top & \Rightarrow & \top \\
    \bot \limp P & \Rightarrow & \top \\
    P \limp \bot & \Rightarrow & \neg P
  \end{array}
</math>
 
Below are the step by step instructions to create an automatic rewrite reasoner:
 
* Create a new plug-in project, e.g. ''org.eventb.contributors.seqprover.autorewrites''. Deselect the plug-in options for "Generating an activator" and "Contribution to the UI".
 
* Add dependency on the project ''org.eventb.core.seqprover''
 
* Add an extension for ''org.eventb.core.seqprover.reasoners'', e.g.


<extension point="org.eventb.core.seqprover.reasoners">
=== Implementing a Tactic ===
  <reasoner
    class="org.eventb.contributors.seqprover.autorewrite.AutoRewrites"
    id="autoRewrites"
    name="%autoRewritesName"/>
</extension>
(add the key autoRewritesName to the plugin.properties accordingly).


* Click on the class attribute of the newly created extension. A dialog appears for new class wizard.
* [[Adding Automatic Tactics | Automatic Tactics]]: Tactics that can be run automatically either as POM Tactics or Post Tactics.


* The abstract implementation of this class is ''org.eventb.internal.core.seqprover.eventbExtensions.rewriters.AbstractAutoRewrites''. Choose this as the Superclass in the new class wizard. (For the moment, the class is internal within the project and subjected to be changed. Clients can make a copy of this class to develop their own implementation).
* [[Adding Manual Tactics | Manual Tactics ]]: Tactics that need to be invoke manually during interactive proofs.


* Finish the wizard and a new implementation for AutoRewrite class is created.


* The implementation can be as follows:


import org.eventb.core.ast.IFormulaRewriter;
[[Category:Developer documentation]]
import org.eventb.internal.core.seqprover.eventbExtensions.rewriters.AbstractAutoRewrites;
[[Category:Rodin Platform]]
public class AutoRewrites extends AbstractAutoRewrites {
[[Category:Proof]]
  public AutoRewrites() {
    super(new AutoRewriterImpl(), true);
  }
  public static String REASONER_ID = "org.evenb.contributors.seqprover.autoRewrites";
  public String getReasonerID() {
    return REASONER_ID;
  }
  @Override
  protected String getDisplayName() {
    return "simplification rewrites";
  }
}
 
The constructor must call the super constructor method ''super(IFormulaRewriter, boolean)'' to specify the formula rewriter to use and the resulting reasoner should hide the source of the rewritten hypothesis or not. Clients need to implement two methods. The first one, namely ''getReasonerID()'', return the string ID of this reasoner. This must be the same ID as declared in the ''plugin.xml'' file (do not forget the project name prefix). The second method is ''getDisplayName()'' which return the display name of the reasoner, which will be used for displaying in the UI.
 
=== Automatic Inference Reasoners ===
 
=== Manual Rewrite Reasoners ===
 
=== Manual Inference Reasoners ===
 
=== General Purpose Reasoners ===
 
== Adding a New Tactic ==

Latest revision as of 10:27, 27 October 2011

The Proof Manager is responsible for constructing proofs and maintaining existing proofs associated with proof obligations.

There are two ways for extending the Proof Manager:

  1. adding a new reasoner.
  1. adding a new tactic.

Adding a New Reasoner

A reasoner is added into the Proof Manager using the extension point org.eventb.core.seqprover.reasoners. Below is an example of how to contribute to the extension point. 

<extension point="org.eventb.core.seqprover.reasoners">
  <reasoner
    class="org.eventb.contributors.seqprover.reasoners.Hyp"
    id="hyp"
    name="%hypName"/>
</extension>

where the name attribute is internationalized.

The above declaration defines a reasoner with a specific id (which will be automatically prefixed by the project name, e.g. org.eventb.contributors.seqprover).

The class attribute must be a valid Java class name which will be used to create an instance of the reasoner. This class must implements org.eventb.core.seqprover.IReasoner interface.

However, most of the time, the developers only need to sub-class one of the abstract implementation, depending on the type of the reasoner. For the implementation purpose, we categorize our reasoners into the following types.

  • Automatic rewrite Reasoners of this type apply some rewriting rules automatically to simplify the input sequent.
  • Manual rewrite Reasoners of this type apply a rewriting rule for a given formula (or sub-formula) in the goal or in one of the hypotheses.
  • General purpose Reasoners that do not fall into the four previous categories.

Please also have a look at How To Evolve Reasoners.

Adding a New Tactic

Adding a reasoner is only a first step in extending the Proof Manager. Reasoners need to be wrapped by Tactics for the Proof Manager to use. Similar to reasoners, there are different types of tactics for implementation purpose.

Implementing a Tactic

  • Automatic Tactics: Tactics that can be run automatically either as POM Tactics or Post Tactics.
  • Manual Tactics : Tactics that need to be invoke manually during interactive proofs.
Retrieved from ‘https://wiki.event-b.org/index.php?title=Extending_the_Proof_Manager&oldid=4788’