Extending the Proof Manager

From Event-B
Revision as of 14:30, 11 September 2008 by imported>Son
Jump to navigationJump to search

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 are 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 Reasoner 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.

Automatic Rewrite 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:


  \begin{array}{rcl}
     \top \limp P & \Rightarrow & P \\
     P \limp \top & \Rightarrow & \top \\
     \bot \limp P & \Rightarrow & \top \\
     P \limp \bot & \Rightarrow & \neg P
  \end{array}

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">
  <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.
  • 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).
  • Finish the wizard and a new implementation for AutoRewrite class is created.
  • The implementation can be as follows:
import org.eventb.core.ast.IFormulaRewriter;

public class AutoRewrites extends AbstractAutoRewrites {

  private static final IFormulaRewriter rewriter = new AutoRewriterImpl();

    public AutoRewrites() {
      super(rewriter, 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