Extending the Proof Manager: Difference between revisions
From Event-B
Jump to navigationJump to search
imported>Son No edit summary |
imported>Son No edit summary |
||
| Line 18: | Line 18: | ||
</extension> | </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. | |||
== Adding a New Tactic == | == Adding a New Tactic == | ||
Revision as of 13:27, 11 September 2008
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:
- adding a new reasoner.
- 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.
