Difference between revisions of "Adding Automatic Rewrite Reasoners"

From Event-B
Jump to navigationJump to search
imported>Son
imported>Nicolas
m
 
(10 intermediate revisions by 4 users not shown)
Line 1: Line 1:
 
{{TOCright}}
 
{{TOCright}}
 +
''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:  
 
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:  
  
Line 14: Line 17:
  
 
== Create the Reasoner ==
 
== Create the 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".
+
* Create a new plug-in project, e.g. ''org.eventb.contributors.seqprover.implrewrites''. Deselect the plug-in options for "Generating an activator" and "Contribution to the UI".
  
 
* Add dependency on the project ''org.eventb.core.seqprover''
 
* Add dependency on the project ''org.eventb.core.seqprover''
Line 22: Line 25:
 
  <extension point="org.eventb.core.seqprover.reasoners">
 
  <extension point="org.eventb.core.seqprover.reasoners">
 
   <reasoner
 
   <reasoner
     class="org.eventb.internal.contributors.seqprover.autorewrites.ImplRewrites"
+
     class="org.eventb.internal.contributors.seqprover.implrewrites.AutoRewrites"
     id="implRewrites"
+
     id="autoRewrites"
     name="%implRewritesName"/>
+
     name="%autoRewritesName"/>
 
  </extension>
 
  </extension>
 
   
 
   
(add the key implRewritesName to the plugin.properties accordingly).
+
(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.
 
* Click on the class attribute of the newly created extension. A dialog appears for new class wizard.
Line 33: Line 36:
 
* 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).
 
* 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 ImplRewrites class is created.
+
* Finish the wizard and a new implementation for AutoRewrites class is created.
  
 
* The implementation can be as follows:
 
* The implementation can be as follows:
  package org.eventb.internal.contributors.seqprover.autorewrites;
+
 
 +
  package org.eventb.internal.contributors.seqprover.implrewrites;
 
   
 
   
 +
import org.eventb.core.seqprover.IReasoner;
 
  import org.eventb.internal.core.seqprover.eventbExtensions.rewriters.AbstractAutoRewrites;
 
  import org.eventb.internal.core.seqprover.eventbExtensions.rewriters.AbstractAutoRewrites;
import org.eventb.core.seqprover.IReasoner;
 
 
   
 
   
  public class ImplRewrites extends AbstractAutoRewrites {
+
  public class AutoRewrites extends AbstractAutoRewrites implements IReasoner {
 
   
 
   
   public ImplRewrites() {
+
   public AutoRewrites() {
     super(new ImplRewriterImpl(), true);
+
     super(new RewriterImpl(), true);
 
   }
 
   }
 
   
 
   
   public static String REASONER_ID = "org.eventb.contributors.seqprover.autorewrites.implRewrites";
+
   public static String REASONER_ID = "org.eventb.contributors.seqprover.implrewrites.autoRewrites";
 
   
 
   
 
   public String getReasonerID() {
 
   public String getReasonerID() {
Line 55: Line 59:
 
   @Override
 
   @Override
 
   protected String getDisplayName() {
 
   protected String getDisplayName() {
     return "implication rewrites";
+
     return "automatic implication rewrites";
 
   }
 
   }
 
   
 
   
Line 63: Line 67:
  
 
What left is to implement the formula rewriter which is used in the constructor of the reasoner. This is very convenient by using [http://tom.loria.fr/ Tom].
 
What left is to implement the formula rewriter which is used in the constructor of the reasoner. This is very convenient by using [http://tom.loria.fr/ Tom].
 +
 +
Note: in order to avoid problems with subsequent reasoner implementation evolutions, it would be wise to implement a [[Versioned Reasoners|versioned reasoner]] (one more simple method).
  
 
== Setting up Tom ==
 
== Setting up Tom ==
Line 68: Line 74:
 
* Create a file named ''build-tom.xml'' within your project. The content of the file looks like this.
 
* Create a file named ''build-tom.xml'' within your project. The content of the file looks like this.
  
  <project name="org.eventb.contributors.seqprover.autorewrites" default="tom" basedir=".">
+
  <project name="org.eventb.contributors.seqprover.implrewrites" default="tom" basedir=".">
 
   <description>
 
   <description>
 
     Generates derived files in the Sequent Prover.
 
     Generates derived files in the Sequent Prover.
Line 80: Line 86:
 
 
 
 
 
   <property name="rewriter.src"
 
   <property name="rewriter.src"
       location="${src}/org/eventb/internal/contributors/seqprover/autorewrites" />
+
       location="${src}/org/eventb/internal/contributors/seqprover/implrewrites" />
 
   
 
   
 
   <target name="init" description="Create the initial time stamp">
 
   <target name="init" description="Create the initial time stamp">
Line 99: Line 105:
 
   
 
   
 
   <target name="clean" description="clean up">
 
   <target name="clean" description="clean up">
     <delete file="${rewriter.src}/ImplRewriterImpl.java" />
+
     <delete file="${rewriter.src}/RewriterImpl.java" />
 
   </target>
 
   </target>
 
 
 
 
Line 114: Line 120:
 
* At the "Targets" tab:
 
* At the "Targets" tab:
 
** Auto Build: Click ''Set Targets'' and choose "tom" from the list.
 
** Auto Build: Click ''Set Targets'' and choose "tom" from the list.
** During a "clean": Click "Set Targets" and choose ''clean'' (unchecked ''tom'').  
+
** During a "clean": Click "Set Targets" and choose ''clean'' (unchecked ''tom'').
  
 
== Implement the Formula Rewriter ==
 
== Implement the Formula Rewriter ==
* Create a Tom file within the same package as the reasoner. In our example, the file should be ''org.eventb.internal.contributors.seqprover.autorewrites.ImplRewriterImpl.t''
+
* Create a Tom file within the same package as the reasoner. In our example, the file should be ''org.eventb.internal.contributors.seqprover.implrewrites.RewriterImpl.t''
  
 
* The content of the file looks like this (for the above rewriting rules).
 
* The content of the file looks like this (for the above rewriting rules).
  
  package org.eventb.internal.contributors.seqprover.autorewrites;
+
  package org.eventb.internal.contributors.seqprover.implrewrites;
 
   
 
   
 
  import java.util.ArrayList;
 
  import java.util.ArrayList;
Line 154: Line 160:
 
   
 
   
 
  @SuppressWarnings("unused")
 
  @SuppressWarnings("unused")
  public class ImplRewriterImpl extends DefaultRewriter {
+
  public class RewriterImpl extends DefaultRewriter {
 
   
 
   
   public ImplRewriterImpl() {
+
   public RewriterImpl() {
 
     super(true, FormulaFactory.getDefault());
 
     super(true, FormulaFactory.getDefault());
 
   }
 
   }
Line 200: Line 206:
 
* For more information about using Tom, you can find from the website for [http://tom.loria.fr/ Tom wiki]. The predefined patterns for Event-B is in ''org.eventb.core.ast'' project at the following location ''/tom/Formula.tom''.
 
* For more information about using Tom, you can find from the website for [http://tom.loria.fr/ Tom wiki]. The predefined patterns for Event-B is in ''org.eventb.core.ast'' project at the following location ''/tom/Formula.tom''.
  
* An extensive example is in the implementation of the Simplification Rewriter in the ''org.eventb.core.seqprover'' project at this location ''org.eventb.internal.core.seqprover.eventbExtensions.rewrites/AutoRewriterImpl.t''
+
* An extensive example is in the implementation of the Simplification Rewriter in the ''org.eventb.core.seqprover'' project at this location ''org.eventb.internal.core.seqprover.eventbExtensions.rewrites/RewriterImpl.t''
  
 
== Modify the Tom Task ==
 
== Modify the Tom Task ==
 
Open the Tom task again (from the Properties of the project).
 
Open the Tom task again (from the Properties of the project).
  
* ''Refresh'' tab: Choose "Refresh resource upon completion", and "Specific resources". Click "Specify Resources" and browse to the location of the folder contains the Tom file. In our example, it will be ''src/org/eventb/internal/contributors/seqprover/autorewrites''
+
* ''Refresh'' tab: Choose "Refresh resource upon completion", and "Specific resources". Click "Specify Resources" and browse to the location of the folder contains the Tom file. In our example, it will be ''src/org/eventb/internal/contributors/seqprover/implrewrites''
  
* ''Build Options'' tab: Click "Specify working set of relevant resources". Click "Specify Resources" and browse to the Tom file, i.e. "AutoRewriterImpl.t".
+
* ''Build Options'' tab: Click "Specify working set of relevant resources". Click "Specify Resources" and browse to the Tom file, i.e. "RewriterImpl.t".
  
 
* Click Apply and OK to close the dialog.
 
* Click Apply and OK to close the dialog.
  
* The Tom Builder should run and generate the Java implementation for AutoRewriterImpl.java in the specified folder.
+
* The Tom Builder should run and generate the Java implementation for RewriterImpl.java in the specified folder.
  
 
== Test the Reasoner ==
 
== Test the Reasoner ==
Line 219: Line 225:
 
Follow the steps below to create a test for declaration of the newly created reasoner.
 
Follow the steps below to create a test for declaration of the newly created reasoner.
  
* Create a test plug-in project, e.g. ''org.eventb.contributors.seqprover.autorewrites.tests''
+
* Create a test plug-in project, e.g. ''org.eventb.contributors.seqprover.implrewrites.tests''
  
* Create dependencies on ''org.eventb.core.seqprover.tests'' and the project under test (in our example, it is ''org.eventb.contributors.seqprover.autorewrites''.
+
* Create dependencies on ''org.eventb.core.seqprover.tests'' and the project under test (in our example, it is ''org.eventb.contributors.seqprover.implrewrites''.
  
* Create a package for the tests, e.g. ''org.eventb.internal.contributors.seqprover.autorewrites.tests''
+
* Create a package for the tests, e.g. ''org.eventb.internal.contributors.seqprover.implrewrites.tests''
  
 
* Create a new class within the newly created package. This class will extend this abstract test class ''org.eventb.core.seqprover.rewriterTests.AbstractAutomaticReasonerTests''.
 
* Create a new class within the newly created package. This class will extend this abstract test class ''org.eventb.core.seqprover.rewriterTests.AbstractAutomaticReasonerTests''.
Line 229: Line 235:
 
* The content of the test class is as follows
 
* The content of the test class is as follows
  
  package org.eventb.internal.contributors.seqprover.autorewrites.tests;
+
  package org.eventb.internal.contributors.seqprover.implrewrites.tests;
 
   
 
   
 
  import org.eventb.core.seqprover.rewriterTests.AbstractAutomaticReasonerTests;
 
  import org.eventb.core.seqprover.rewriterTests.AbstractAutomaticReasonerTests;
 
   
 
   
  public class ImplRewritesReasonerTests extends AbstractAutomaticReasonerTests {
+
  public class AutoReasonerTests extends AbstractAutomaticReasonerTests {
 
   
 
   
 
   @Override
 
   @Override
Line 253: Line 259:
 
   @Override
 
   @Override
 
   public String getReasonerID() {
 
   public String getReasonerID() {
     return "org.eventb.contributors.seqprover.autorewrites.implRewrites";
+
     return "org.eventb.contributors.seqprover.implrewrites.autoRewrites";
 
   }
 
   }
 
   
 
   
Line 259: Line 265:
  
 
* As mentioned before, clients only need to test if the reasoner ID has been declared correctly. This is done by implemented the method ''String getReasonerID()'' which should return the correct reasoner ID.
 
* As mentioned before, clients only need to test if the reasoner ID has been declared correctly. This is done by implemented the method ''String getReasonerID()'' which should return the correct reasoner ID.
 +
 +
* Run AutoReasonerTests as a JUnit Plug-in Test.
  
 
=== Test the Formula Rewriter ===
 
=== Test the Formula Rewriter ===
 
In order to test the formula rewriter, the formula rewriter implementation needs to be visible to the test project.
 
In order to test the formula rewriter, the formula rewriter implementation needs to be visible to the test project.
  
* Open plugin.xml of the project undertest, e.g. ''org.eventb.contributors.seqprover.autorewrites''
+
* Open plugin.xml of the project undertest, e.g. ''org.eventb.contributors.seqprover.implrewrites''
  
 
* Click on ''Runtime'' tab.
 
* Click on ''Runtime'' tab.
  
* Export the package ''org.eventb.internal.contributors.seqprover.autorewrites''.
+
* Export the package ''org.eventb.internal.contributors.seqprover.implrewrites''.
  
* For package visibility, choose ''hidden from all plug-in except'' the test project, e.g. ''org.eventb.internal.contributors.seqprover.autorewrites.tests''.
+
* For package visibility, choose ''hidden from all plug-in except'' the test project, e.g. ''org.eventb.internal.contributors.seqprover.implrewrites.tests''.
  
 
Now, create a tests class for testing the formula rewriter.
 
Now, create a tests class for testing the formula rewriter.
Line 279: Line 287:
 
* The implementation looks like this.
 
* The implementation looks like this.
  
  package org.eventb.internal.contributors.seqprover.autorewrites.tests;
+
  package org.eventb.internal.contributors.seqprover.implrewrites.tests;
 
   
 
   
 
  import org.eventb.core.ast.IFormulaRewriter;
 
  import org.eventb.core.ast.IFormulaRewriter;
 
  import org.eventb.core.seqprover.rewriterTests.AbstractFormulaRewriterTests;
 
  import org.eventb.core.seqprover.rewriterTests.AbstractFormulaRewriterTests;
  import org.eventb.internal.contributors.seqprover.autorewrites.ImplRewriterImpl;
+
  import org.eventb.internal.contributors.seqprover.implrewrites.RewriterImpl;
 
  import org.junit.Test;
 
  import org.junit.Test;
 
   
 
   
  public class ImplRewriterTests extends AbstractFormulaRewriterTests {
+
  public class AutoRewriterTests extends AbstractFormulaRewriterTests {
 
   // The automatic rewriter for testing.
 
   // The automatic rewriter for testing.
   private static final IFormulaRewriter rewriter = new ImplRewriterImpl();
+
   private static final IFormulaRewriter rewriter = new RewriterImpl();
 
 
 
 
 
   /**
 
   /**
Line 296: Line 304:
 
     * rewriter.
 
     * rewriter.
 
     */
 
     */
   public ImplRewriterTests() {
+
   public AutoRewriterTests() {
 
     super(rewriter);
 
     super(rewriter);
 
   }
 
   }
 
+
 
   /**
 
   /**
 
     * Tests for rewriting implication.
 
     * Tests for rewriting implication.
Line 316: Line 324:
 
   
 
   
 
  }
 
  }
 +
 +
* Run AutoRewriterTests as a JUnit Plug-in Test.
 +
 +
* The constructor should call the super constructor with an instance of the rewriter under test.
 +
 +
* In this case, we want to test the correctness of the rewriter using the method ''predicateTest(String expected, String input)''. Both these string must be in the Event-B mathematical format and must be able to type-checked. In order to enter the formula, users are suggested to use the [[Event-B Keyboard View]].
 +
 +
* There is a similar method for expression test ''expressionTest(String expected, String input)''.
 +
 +
* More instructions about how to use the method predicateTest  and expressionTest (along with some other utility methods) can be found in ''org.eventb.core.seqprover.rewriterTests.AbstractFormulaRewriterTests'' class.
 +
 +
 +
 +
[[Category:Developer documentation]]
 +
[[Category:Rodin Platform]]

Latest revision as of 17:33, 24 November 2010

Please also have a look at 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:


  \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 the Reasoner

  • Create a new plug-in project, e.g. org.eventb.contributors.seqprover.implrewrites. 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 for our implication rewrite reasoner, e.g.
<extension point="org.eventb.core.seqprover.reasoners">
  <reasoner
    class="org.eventb.internal.contributors.seqprover.implrewrites.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 AutoRewrites class is created.
  • The implementation can be as follows:
package org.eventb.internal.contributors.seqprover.implrewrites;

import org.eventb.core.seqprover.IReasoner;
import org.eventb.internal.core.seqprover.eventbExtensions.rewriters.AbstractAutoRewrites;

public class AutoRewrites extends AbstractAutoRewrites implements IReasoner {

  public AutoRewrites() {
    super(new RewriterImpl(), true);
  }

  public static String REASONER_ID = "org.eventb.contributors.seqprover.implrewrites.autoRewrites";

  public String getReasonerID() {
    return REASONER_ID;
  }

  @Override
  protected String getDisplayName() {
    return "automatic implication 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.

What left is to implement the formula rewriter which is used in the constructor of the reasoner. This is very convenient by using Tom.

Note: in order to avoid problems with subsequent reasoner implementation evolutions, it would be wise to implement a versioned reasoner (one more simple method).

Setting up Tom

  • Create a file named build-tom.xml within your project. The content of the file looks like this.
<project name="org.eventb.contributors.seqprover.implrewrites" default="tom" basedir=".">
  <description>
    Generates derived files in the Sequent Prover.
  </description>

  <property name="src" location="src" />

  <property name="org.eventb.core.ast.home" location="../org.eventb.core.ast" />
  <import file="${org.eventb.core.ast.home}/tom/tom-task.xml"/>
	
  <property name="rewriter.src"
      location="${src}/org/eventb/internal/contributors/seqprover/implrewrites" />

  <target name="init" description="Create the initial time stamp">
    <tstamp />
  </target>

  <target name="tom" depends="init"
      description="Launch tom for all files">
    <tom config="${tom.home}/Tom.xml"
        srcdir="${src}"
        destdir="${src}"
        options="-I ${org.eventb.core.ast.home}/tom --static"
        pretty="true"
        optimize="true">
      <include name="**/*.t" />
    </tom>
  </target>

  <target name="clean" description="clean up">
    <delete file="${rewriter.src}/RewriterImpl.java" />
  </target>
	
</project>

The best way to create this file is to copy from org.eventb.core.seqprover project, and modify this accordingly.

  • Right click on the name of your project and choose Properties.
  • Choose "Builders", then click on "New" and choose "Ant Build" and click OK. A dialog will open for new builder wizard.
  • At the "Main" tab:
    • Enter the name of the builder, e.g. Tom Builder.
    • Buildfile: Browse Workspace to your build-tom.xml.
    • Base Directory: Variables and choose build_project.
  • At the "Targets" tab:
    • Auto Build: Click Set Targets and choose "tom" from the list.
    • During a "clean": Click "Set Targets" and choose clean (unchecked tom).

Implement the Formula Rewriter

  • Create a Tom file within the same package as the reasoner. In our example, the file should be org.eventb.internal.contributors.seqprover.implrewrites.RewriterImpl.t
  • The content of the file looks like this (for the above rewriting rules).
package org.eventb.internal.contributors.seqprover.implrewrites;

import java.util.ArrayList;
import java.util.Collection;
import java.math.BigInteger;

import org.eventb.core.ast.AssociativeExpression;
import org.eventb.core.ast.AssociativePredicate;
import org.eventb.core.ast.AtomicExpression;
import org.eventb.core.ast.BinaryExpression;
import org.eventb.core.ast.BinaryPredicate;
import org.eventb.core.ast.BoolExpression;
import org.eventb.core.ast.BoundIdentDecl;
import org.eventb.core.ast.BoundIdentifier;
import org.eventb.core.ast.DefaultRewriter;
import org.eventb.core.ast.Expression;
import org.eventb.core.ast.Formula;
import org.eventb.core.ast.FormulaFactory;
import org.eventb.core.ast.FreeIdentifier;
import org.eventb.core.ast.Identifier;
import org.eventb.core.ast.IntegerLiteral;
import org.eventb.core.ast.LiteralPredicate;
import org.eventb.core.ast.Predicate;
import org.eventb.core.ast.QuantifiedExpression;
import org.eventb.core.ast.QuantifiedPredicate;
import org.eventb.core.ast.RelationalPredicate;
import org.eventb.core.ast.SetExtension;
import org.eventb.core.ast.SimplePredicate;
import org.eventb.core.ast.UnaryExpression;
import org.eventb.core.ast.UnaryPredicate;
import org.eventb.core.seqprover.eventbExtensions.Lib;

@SuppressWarnings("unused")
public class RewriterImpl extends DefaultRewriter {

  public RewriterImpl() {
    super(true, FormulaFactory.getDefault());
  }

  %include {Formula.tom}

  @Override
  public Predicate rewrite(BinaryPredicate predicate) {
    %match (Predicate predicate) {
      /**
       * Implication 1: ⊤ ⇒ P == P
       */
      Limp(BTRUE(), P) -> {
        return `P;
      }

      /**
       * Implication 2: ⊥ ⇒ P == ⊤
       */
      Limp(BFALSE(), _) -> {
        return Lib.True;
      }

      /**
       * Implication 3: P ⇒ ⊤ == ⊤
       */
      Limp(_, BTRUE()) -> {
        return predicate.getRight();
      }
    	
      /**
       * Implication 4: P ⇒ ⊥ == ¬P
       */
      Limp(P, BFALSE()) -> {
        return Lib.makeNeg(`P);
      }
    }

    return predicate;
  }
}
  • For more information about using Tom, you can find from the website for Tom wiki. The predefined patterns for Event-B is in org.eventb.core.ast project at the following location /tom/Formula.tom.
  • An extensive example is in the implementation of the Simplification Rewriter in the org.eventb.core.seqprover project at this location org.eventb.internal.core.seqprover.eventbExtensions.rewrites/RewriterImpl.t

Modify the Tom Task

Open the Tom task again (from the Properties of the project).

  • Refresh tab: Choose "Refresh resource upon completion", and "Specific resources". Click "Specify Resources" and browse to the location of the folder contains the Tom file. In our example, it will be src/org/eventb/internal/contributors/seqprover/implrewrites
  • Build Options tab: Click "Specify working set of relevant resources". Click "Specify Resources" and browse to the Tom file, i.e. "RewriterImpl.t".
  • Click Apply and OK to close the dialog.
  • The Tom Builder should run and generate the Java implementation for RewriterImpl.java in the specified folder.

Test the Reasoner

The abstract automatic rewriting reasoners has been tested, so clients only need to test if the reasoner has been declared correctly (testing the reasoner ID), and the formula rewriter used for this reasoner has been implemented correctly.

Test the Declaration

Follow the steps below to create a test for declaration of the newly created reasoner.

  • Create a test plug-in project, e.g. org.eventb.contributors.seqprover.implrewrites.tests
  • Create dependencies on org.eventb.core.seqprover.tests and the project under test (in our example, it is org.eventb.contributors.seqprover.implrewrites.
  • Create a package for the tests, e.g. org.eventb.internal.contributors.seqprover.implrewrites.tests
  • Create a new class within the newly created package. This class will extend this abstract test class org.eventb.core.seqprover.rewriterTests.AbstractAutomaticReasonerTests.
  • The content of the test class is as follows
package org.eventb.internal.contributors.seqprover.implrewrites.tests;

import org.eventb.core.seqprover.rewriterTests.AbstractAutomaticReasonerTests;

public class AutoReasonerTests extends AbstractAutomaticReasonerTests {

  @Override
  protected SuccessfulTest[] getSuccessfulTests() {
    // No need to test this. This should be guaranteed by testing the
    // abstract automatic rewrite reasoner and the formula rewriter itself.
    return new SuccessfulTest [] {
    };
  }

  @Override
  protected String[] getUnsuccessfulTests() {
    // No need to test this. This should be guaranteed by testing the
    // abstract automatic rewrite reasoner and the formula rewriter itself.
    return new String [] {
    };	
  }

  @Override
  public String getReasonerID() {
    return "org.eventb.contributors.seqprover.implrewrites.autoRewrites";
  }

}
  • As mentioned before, clients only need to test if the reasoner ID has been declared correctly. This is done by implemented the method String getReasonerID() which should return the correct reasoner ID.
  • Run AutoReasonerTests as a JUnit Plug-in Test.

Test the Formula Rewriter

In order to test the formula rewriter, the formula rewriter implementation needs to be visible to the test project.

  • Open plugin.xml of the project undertest, e.g. org.eventb.contributors.seqprover.implrewrites
  • Click on Runtime tab.
  • Export the package org.eventb.internal.contributors.seqprover.implrewrites.
  • For package visibility, choose hidden from all plug-in except the test project, e.g. org.eventb.internal.contributors.seqprover.implrewrites.tests.

Now, create a tests class for testing the formula rewriter.

  • If you have not create a test project and test package, follow the first few steps in the previous section.
  • Create a new test class in the test package. This class extends org.eventb.core.seqprover.rewriterTests.AbstractFormulaRewriterTests.
  • The implementation looks like this.
package org.eventb.internal.contributors.seqprover.implrewrites.tests;

import org.eventb.core.ast.IFormulaRewriter;
import org.eventb.core.seqprover.rewriterTests.AbstractFormulaRewriterTests;
import org.eventb.internal.contributors.seqprover.implrewrites.RewriterImpl;
import org.junit.Test;

public class AutoRewriterTests extends AbstractFormulaRewriterTests {
  // The automatic rewriter for testing.
  private static final IFormulaRewriter rewriter = new RewriterImpl();
	
  /**
   * Constructor.
   * 
   * Create an abstract formula rewriter test with the input is the automatic
   * rewriter.
   */
  public AutoRewriterTests() {
    super(rewriter);
  }

  /**
   * Tests for rewriting implication.
   */
  @Test
  public void testImplRewrite() {
    // true => P  ==  P
    predicateTest("x = 1", "⊤ ⇒ x = 1");
    // P => true  ==  true
    predicateTest("⊤", "x = 1 ⇒ ⊤");
    // false => P  ==  true
    predicateTest("⊤", "⊥ ⇒ x = 1");
    // P => false  ==  not(P)
    predicateTest("¬(x = 1)", "x = 1 ⇒ ⊥");
  }

}
  • Run AutoRewriterTests as a JUnit Plug-in Test.
  • The constructor should call the super constructor with an instance of the rewriter under test.
  • In this case, we want to test the correctness of the rewriter using the method predicateTest(String expected, String input). Both these string must be in the Event-B mathematical format and must be able to type-checked. In order to enter the formula, users are suggested to use the Event-B Keyboard View.
  • There is a similar method for expression test expressionTest(String expected, String input).
  • More instructions about how to use the method predicateTest and expressionTest (along with some other utility methods) can be found in org.eventb.core.seqprover.rewriterTests.AbstractFormulaRewriterTests class.