Difference between revisions of "Adding Automatic Inference Reasoners"
imported>Son |
imported>Nicolas m |
||
(11 intermediate revisions by 3 users not shown) | |||
Line 1: | Line 1: | ||
+ | {{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 applies an inference rule to the input sequent. As an example, consider the following inference rule (called ''IMP_R''). | Beside the input sequent, reasoners of this type does not have any extra input and automatically applies an inference rule to the input sequent. As an example, consider the following inference rule (called ''IMP_R''). | ||
{{InfRule | IMP_R | <math>\frac{H, P \vdash Q}{H \vdash P \limp Q}</math>}} | {{InfRule | IMP_R | <math>\frac{H, P \vdash Q}{H \vdash P \limp Q}</math>}} | ||
− | == | + | == Declare the Reasoner == |
* Create a new plug-in project, e.g. ''org.eventb.contributors.seqprover.implinference''. 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.implinference''. Deselect the plug-in options for "Generating an activator" and "Contribution to the UI". | ||
Line 20: | Line 24: | ||
* We will use Tom to implement the reasoner class itself. | * We will use Tom to implement the reasoner class itself. | ||
+ | |||
+ | == Implement the Reasoner == | ||
+ | The following steps is for implementing the reasoner using Tom. | ||
+ | |||
+ | * Create a package within the ''src'' folder of the project with the name ''org.eventb.internal.contributors.seqprover.implinference''. | ||
+ | |||
+ | * Create a Tom file within the newly created package with the name ''AutoInference.t''. | ||
+ | |||
+ | * The content of the Tom file looks like this. | ||
+ | |||
+ | package org.eventb.internal.contributors.seqprover.implinference; | ||
+ | |||
+ | import java.math.BigInteger; | ||
+ | import java.util.ArrayList; | ||
+ | import java.util.Collection; | ||
+ | import java.util.List; | ||
+ | import java.util.Set; | ||
+ | import java.util.HashSet; | ||
+ | |||
+ | 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.DefaultFilter; | ||
+ | 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.IPosition; | ||
+ | import org.eventb.core.ast.LiteralPredicate; | ||
+ | import org.eventb.core.ast.PowerSetType; | ||
+ | import org.eventb.core.ast.Predicate; | ||
+ | import org.eventb.core.ast.ProductType; | ||
+ | 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.Type; | ||
+ | import org.eventb.core.ast.UnaryExpression; | ||
+ | import org.eventb.core.ast.UnaryPredicate; | ||
+ | import org.eventb.core.seqprover.eventbExtensions.Tactics; | ||
+ | import org.eventb.core.seqprover.IProverSequent; | ||
+ | import org.eventb.core.seqprover.IHypAction; | ||
+ | import org.eventb.core.seqprover.ProverFactory; | ||
+ | import org.eventb.core.seqprover.SequentProver; | ||
+ | import org.eventb.core.seqprover.IProofRule.IAntecedent; | ||
+ | import org.eventb.core.seqprover.eventbExtensions.Lib; | ||
+ | import org.eventb.core.seqprover.eventbExtensions.Tactics; | ||
+ | import org.eventb.internal.core.seqprover.eventbExtensions.AbstractAutoInference; | ||
+ | |||
+ | /** | ||
+ | * Basic implementation for "automatic implication inference" | ||
+ | */ | ||
+ | @SuppressWarnings("unused") | ||
+ | public class AutoInference extends AbstractAutoInference { | ||
+ | |||
+ | %include {Formula.tom} | ||
+ | |||
+ | public String getReasonerID() { | ||
+ | return "org.eventb.contributors.seqprover.implinference.autoInference"; | ||
+ | } | ||
+ | |||
+ | @Override | ||
+ | protected String getDisplayName() { | ||
+ | return "Automatic deduction"; | ||
+ | } | ||
+ | |||
+ | @Override | ||
+ | protected IAntecedent[] getAntecedents(IProverSequent seq) { | ||
+ | Predicate goal = seq.goal(); | ||
+ | |||
+ | Predicate P = null; | ||
+ | Predicate Q = null; | ||
+ | %match (Predicate goal) { | ||
+ | |||
+ | /** | ||
+ | * Deduction: | ||
+ | * H, P |- Q | ||
+ | * ----------- | ||
+ | * H |- P => Q | ||
+ | */ | ||
+ | Limp(PP, QQ) -> { | ||
+ | P = `PP; | ||
+ | Q = `QQ; | ||
+ | } | ||
+ | |||
+ | } | ||
+ | |||
+ | if (P == null) | ||
+ | return null; | ||
+ | |||
+ | // There will be 1 antecidents | ||
+ | IAntecedent[] antecidents = new IAntecedent[1]; | ||
+ | |||
+ | // Added hypothesis P | ||
+ | Set<Predicate> addedHyps = new HashSet<Predicate>(1); | ||
+ | addedHyps.add(P); | ||
+ | // Select the new hypothesis P | ||
+ | IHypAction hypAction = ProverFactory.makeSelectHypAction(addedHyps); | ||
+ | antecidents[0] = ProverFactory.makeAntecedent(Q, addedHyps, hypAction); | ||
+ | |||
+ | return antecidents; | ||
+ | } | ||
+ | |||
+ | } | ||
+ | |||
+ | * The implementation is based on ''org.eventb.internal.core.seqprover.eventbExtensions.AbstractAutoInference''. (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). | ||
+ | |||
+ | * Clients need to implement first the two methods to return the reasoner id, ''getReasonerID()'', and return the display name, ''getDisplayName()''. | ||
+ | |||
+ | * Moreover, clients need to implement the method for getting the actual antecedents ''getAntecedents(IProverSequent seq)'' | ||
+ | ** The input of the method is the sequent. | ||
+ | ** The method return the list of antecedents to implement the inference rule. | ||
+ | ** Tom is used here to do pattern matching. In our case, match the goal with <math>P \limp Q</math>. | ||
+ | ** Methods for construct hypothesis actions, antecedent, etc. can be found in class ''org.eventb.core.seqprover.ProverFactory''. | ||
+ | |||
+ | 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 == | ||
+ | * 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> | ||
+ | |||
+ | <!-- set global properties for this build --> | ||
+ | <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="inference.src" | ||
+ | location="${src}/org/eventb/internal/contributors/seqprover/implinference" /> | ||
+ | |||
+ | <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="${inference.src}/AutoInference.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''). | ||
+ | |||
+ | * At the ''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/implinference'' | ||
+ | |||
+ | * At the ''Build Options'' tab: Click "Specify working set of relevant resources". Click "Specify Resources" and browse to the Tom file, i.e. "AutoInference.t". | ||
+ | |||
+ | * Click Apply and OK to close the dialog. | ||
+ | |||
+ | * The Tom Builder should run and generate the Java implementation for AutoInference.java in the specified folder. | ||
+ | |||
+ | == Test the 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.implinference.tests'' | ||
+ | |||
+ | * Create dependencies on ''org.eventb.core.seqprover.tests'' and the project under test (in our example, it is ''org.eventb.contributors.seqprover.implinference''. | ||
+ | |||
+ | * Create a package for the tests, e.g. ''org.eventb.internal.contributors.seqprover.implinference.tests'' | ||
+ | |||
+ | * Create a new class within the newly created package. This class will extend this abstract test class ''org.eventb.core.seqprover.eventbExtentionTests.AbstractAutoInferenceTests''. | ||
+ | |||
+ | * The content of the test class is as follows | ||
+ | |||
+ | package org.evenb.internal.contributors.seqprover.implinference.tests; | ||
+ | |||
+ | import org.eventb.core.seqprover.eventbExtentionTests.AbstractAutoInferenceTests; | ||
+ | |||
+ | public class AutoInferenceTests extends AbstractAutoInferenceTests { | ||
+ | |||
+ | @Override | ||
+ | protected SuccessfulTest[] getSuccessfulTests() { | ||
+ | return new SuccessfulTest[] { | ||
+ | new SuccessfulTest(" z = 3 ;H; z = 3 ;S; |- x = 1 ⇒ y = 2", "{z=ℤ, y=ℤ, x=ℤ}[z=3][][x=1] |- y=2"), | ||
+ | new SuccessfulTest(" z = 3 ;H; ;S; z = 3 |- x = 1 ⇒ y = 2", "{z=ℤ, y=ℤ, x=ℤ}[][][z=3, x=1] |- y=2") | ||
+ | }; | ||
+ | } | ||
+ | |||
+ | @Override | ||
+ | protected String[] getUnsuccessfulTests() { | ||
+ | return new String[] { | ||
+ | "x = 1 ⇒ y = 2 ;H; x = 1 ⇒ y = 2 ;S; |- z = 3", | ||
+ | "x = 1 ⇒ y = 2 ;H; ;S; x = 1 ⇒ y = 2 |- z = 3", | ||
+ | "x = 1 ⇒ y = 2 ;H; ;S; |- z = 3", | ||
+ | "z = 2 ;H; z = 2 ;S; |- z = 3 ∧ (x = 1 ⇒ y = 2)", | ||
+ | "z = 2 ;H; ;S; z = 2 |- z = 3 ∧ (x = 1 ⇒ y = 2)", | ||
+ | "z = 2 ;H; ;S; |- z = 3 ∧ (x = 1 ⇒ y = 2)" | ||
+ | }; | ||
+ | } | ||
+ | |||
+ | @Override | ||
+ | public String getReasonerID() { | ||
+ | return "org.eventb.contributors.seqprover.implinference.autoInference"; | ||
+ | } | ||
+ | |||
+ | } | ||
+ | |||
+ | * Firstly, by implementing the method ''getReasonerID()'', clients test the declaration of the reasoner. | ||
+ | |||
+ | * Secondly, by implementing the method ''getSuccessfulTests()'', clients test the successful application of the reasoner. | ||
+ | ** The method return a list of ''SuccessfulTest''. | ||
+ | ** The constructor of ''SuccessfulTest'' has two arguments: A string represent the input sequent and a string to represent the output sequents. | ||
+ | ** The format of these sequents can be found in the class ''AbstractAutoInferenceTests''. | ||
+ | |||
+ | * Lastly, by implementing the method ''getUnsuccessfulTests()'', clients test the reasoner against invalid input. | ||
+ | ** The method return a list of strings. | ||
+ | ** Each string represent an invalid input sequent for the reasoner. | ||
+ | |||
+ | [[Category:Developer documentation]] | ||
+ | [[Category:Rodin Platform]] |
Latest revision as of 17:34, 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 applies an inference rule to the input sequent. As an example, consider the following inference rule (called IMP_R).
![]() |
IMP_R |
Declare the Reasoner
- Create a new plug-in project, e.g. org.eventb.contributors.seqprover.implinference. 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.implinference.AutoInference" id="autoInference" name="%autoInferenceName"/> </extension>
(add the key autoInferenceName to the plugin.properties accordingly).
- We will use Tom to implement the reasoner class itself.
Implement the Reasoner
The following steps is for implementing the reasoner using Tom.
- Create a package within the src folder of the project with the name org.eventb.internal.contributors.seqprover.implinference.
- Create a Tom file within the newly created package with the name AutoInference.t.
- The content of the Tom file looks like this.
package org.eventb.internal.contributors.seqprover.implinference; import java.math.BigInteger; import java.util.ArrayList; import java.util.Collection; import java.util.List; import java.util.Set; import java.util.HashSet; 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.DefaultFilter; 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.IPosition; import org.eventb.core.ast.LiteralPredicate; import org.eventb.core.ast.PowerSetType; import org.eventb.core.ast.Predicate; import org.eventb.core.ast.ProductType; 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.Type; import org.eventb.core.ast.UnaryExpression; import org.eventb.core.ast.UnaryPredicate; import org.eventb.core.seqprover.eventbExtensions.Tactics; import org.eventb.core.seqprover.IProverSequent; import org.eventb.core.seqprover.IHypAction; import org.eventb.core.seqprover.ProverFactory; import org.eventb.core.seqprover.SequentProver; import org.eventb.core.seqprover.IProofRule.IAntecedent; import org.eventb.core.seqprover.eventbExtensions.Lib; import org.eventb.core.seqprover.eventbExtensions.Tactics; import org.eventb.internal.core.seqprover.eventbExtensions.AbstractAutoInference; /** * Basic implementation for "automatic implication inference" */ @SuppressWarnings("unused") public class AutoInference extends AbstractAutoInference { %include {Formula.tom} public String getReasonerID() { return "org.eventb.contributors.seqprover.implinference.autoInference"; } @Override protected String getDisplayName() { return "Automatic deduction"; } @Override protected IAntecedent[] getAntecedents(IProverSequent seq) { Predicate goal = seq.goal(); Predicate P = null; Predicate Q = null; %match (Predicate goal) { /** * Deduction: * H, P |- Q * ----------- * H |- P => Q */ Limp(PP, QQ) -> { P = `PP; Q = `QQ; } } if (P == null) return null; // There will be 1 antecidents IAntecedent[] antecidents = new IAntecedent[1]; // Added hypothesis P Set<Predicate> addedHyps = new HashSet<Predicate>(1); addedHyps.add(P); // Select the new hypothesis P IHypAction hypAction = ProverFactory.makeSelectHypAction(addedHyps); antecidents[0] = ProverFactory.makeAntecedent(Q, addedHyps, hypAction); return antecidents; } }
- The implementation is based on org.eventb.internal.core.seqprover.eventbExtensions.AbstractAutoInference. (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).
- Clients need to implement first the two methods to return the reasoner id, getReasonerID(), and return the display name, getDisplayName().
- Moreover, clients need to implement the method for getting the actual antecedents getAntecedents(IProverSequent seq)
- The input of the method is the sequent.
- The method return the list of antecedents to implement the inference rule.
- Tom is used here to do pattern matching. In our case, match the goal with
.
- Methods for construct hypothesis actions, antecedent, etc. can be found in class org.eventb.core.seqprover.ProverFactory.
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="inference.src" location="${src}/org/eventb/internal/contributors/seqprover/implinference" /> <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="${inference.src}/AutoInference.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).
- At the 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/implinference
- At the Build Options tab: Click "Specify working set of relevant resources". Click "Specify Resources" and browse to the Tom file, i.e. "AutoInference.t".
- Click Apply and OK to close the dialog.
- The Tom Builder should run and generate the Java implementation for AutoInference.java in the specified folder.
Test the 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.implinference.tests
- Create dependencies on org.eventb.core.seqprover.tests and the project under test (in our example, it is org.eventb.contributors.seqprover.implinference.
- Create a package for the tests, e.g. org.eventb.internal.contributors.seqprover.implinference.tests
- Create a new class within the newly created package. This class will extend this abstract test class org.eventb.core.seqprover.eventbExtentionTests.AbstractAutoInferenceTests.
- The content of the test class is as follows
package org.evenb.internal.contributors.seqprover.implinference.tests; import org.eventb.core.seqprover.eventbExtentionTests.AbstractAutoInferenceTests; public class AutoInferenceTests extends AbstractAutoInferenceTests { @Override protected SuccessfulTest[] getSuccessfulTests() { return new SuccessfulTest[] { new SuccessfulTest(" z = 3 ;H; z = 3 ;S; |- x = 1 ⇒ y = 2", "{z=ℤ, y=ℤ, x=ℤ}[z=3][][x=1] |- y=2"), new SuccessfulTest(" z = 3 ;H; ;S; z = 3 |- x = 1 ⇒ y = 2", "{z=ℤ, y=ℤ, x=ℤ}[][][z=3, x=1] |- y=2") }; } @Override protected String[] getUnsuccessfulTests() { return new String[] { "x = 1 ⇒ y = 2 ;H; x = 1 ⇒ y = 2 ;S; |- z = 3", "x = 1 ⇒ y = 2 ;H; ;S; x = 1 ⇒ y = 2 |- z = 3", "x = 1 ⇒ y = 2 ;H; ;S; |- z = 3", "z = 2 ;H; z = 2 ;S; |- z = 3 ∧ (x = 1 ⇒ y = 2)", "z = 2 ;H; ;S; z = 2 |- z = 3 ∧ (x = 1 ⇒ y = 2)", "z = 2 ;H; ;S; |- z = 3 ∧ (x = 1 ⇒ y = 2)" }; } @Override public String getReasonerID() { return "org.eventb.contributors.seqprover.implinference.autoInference"; } }
- Firstly, by implementing the method getReasonerID(), clients test the declaration of the reasoner.
- Secondly, by implementing the method getSuccessfulTests(), clients test the successful application of the reasoner.
- The method return a list of SuccessfulTest.
- The constructor of SuccessfulTest has two arguments: A string represent the input sequent and a string to represent the output sequents.
- The format of these sequents can be found in the class AbstractAutoInferenceTests.
- Lastly, by implementing the method getUnsuccessfulTests(), clients test the reasoner against invalid input.
- The method return a list of strings.
- Each string represent an invalid input sequent for the reasoner.