Sequent Prover Developer Guide - Revision history

imported>Pascal: /* Font */

2010-06-17T09:48:59Z

Font

← Older revision		Revision as of 09:48, 17 June 2010
Line 32:		Line 32:
	</extension>		</extension>

	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 name is an externalised string which is used for display purpose.		The above declaration defines a reasoner with a specific id (which will be automatically prefixed by the project name, e.g. <tt>org.eventb.contributors.seqprover</tt>). The name is an externalised string which is used for display purpose.

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

imported>Nicolas: A few small corrections and additional links.

2010-03-04T14:04:02Z

A few small corrections and additional links.

Show changes

imported>Pascal at 10:29, 19 February 2010

2010-02-19T10:29:30Z

Show changes

imported>Pascal: Sequent Prover User Guide moved to Sequent Prover Developer Guide

2010-02-19T10:27:28Z

Sequent Prover User Guide moved to Sequent Prover Developer Guide

← Older revision	Revision as of 10:27, 19 February 2010
(No difference)

imported>Pascal: /* Post-tactics */

2010-02-19T10:26:02Z

Post-tactics

← Older revision		Revision as of 10:26, 19 February 2010
Line 325:		Line 325:
	Once declared as a POM tactic, the information about the tactic will appear in the preferences for the POM tactic and the users of the platform. However, this tactic will not be a default POM tactic and the users must change the preferences to enable this tactic.		Once declared as a POM tactic, the information about the tactic will appear in the preferences for the POM tactic and the users of the platform. However, this tactic will not be a default POM tactic and the users must change the preferences to enable this tactic.

	=== Post-tactics ===		=== Adding a Post Tactic ===
			Post tactics are tactics that are run after every manual proof steps in interactive mode. Only automatic tactics (See [[#Tactics \| tactics]]) can be declared as post tactics.

			Post tactics are added using the extension point <tt>org.eventb.core.postTactic</tt>. An example is as follows:

			<extension point="org.eventb.core.postTactics">
			<tactic id="org.eventb.core.seqprover.trueGoalTac"/>
			</extension>

			Each tactic element only contains an attribute id which must be a valid tactic ID (including the project prefix) as declared using the <tt>org.eventb.core.seqprover.autoTactics</tt> extension point.

			Once declared as a post tactic, the information about the tactic will appear in the preferences for the post tactic and the users of the platform. However, this tactic will not be a default post tactic and the users must change the preferences to enable this tactic.

	= Reference =		= Reference =

imported>Pascal: /* POM Tactics */

2010-02-19T10:23:51Z

POM Tactics

← Older revision		Revision as of 10:23, 19 February 2010
Line 312:		Line 312:

	== Event-B Tactics ==		== Event-B Tactics ==
	=== POM Tactics ===		=== Adding a POM Tactic ===
			POM tactics are tactics that are run by the auto POM. Only automatic tactics (See [[#Tactics \| tactics]]) can be declared as POM tactics.

			POM tactics are added using the extension point <tt>org.eventb.core.pomTactic</tt>. An example is given below:

			<extension point="org.eventb.core.pomTactics">
			<tactic id="org.eventb.core.seqprover.trueGoalTac"/>
			</extension>

			Each tactic element only contains an attribute id, which must be a valid tactic ID (including the project prefix) as declared using the <tt>org.eventb.core.seqprover.autoTactics</tt> extension point.

			Once declared as a POM tactic, the information about the tactic will appear in the preferences for the POM tactic and the users of the platform. However, this tactic will not be a default POM tactic and the users must change the preferences to enable this tactic.

	=== Post-tactics ===		=== Post-tactics ===

imported>Pascal: /* Tactics */

2010-02-19T10:19:18Z

Tactics

← Older revision		Revision as of 10:19, 19 February 2010
Line 273:		Line 273:

	=== Tactics ===		=== Tactics ===
			==== Concepts ====
			Tactics provide a way to structure strategic or heuristic knowledge about proof search. They provide control structures to call [[#Reasoners \|reasoners]] or other tactics to make modifications to the [[#Proof_Trees \| proof trees]]. In the Rodin platform, the users are dealing with tactics, not reasoners.

			A tactic can just be the wrapper around a reasoner, but it can be more complicated by combining different tactics.

			===== Adding a tactic =====
			Tactics are divided into two classes: automatic and manual tactics.

			====== Automatic Tactics ======
			A reasoner is added into the Event-B sequent prover using the extension point <tt>org.eventb.core.seqprover.autoTactics</tt>.

			<extension point="org.eventb.core.seqprover.autoTactics">
			<autoTactic
			class="org.eventb.contributors.seqprover.TrueGoalTac"
			description="%trueGoalTacDesc"
			id="trueGoalTac"
			name="%trueGoalTacName">
			</autoTactic>
			</extension>

			The above declaration defines an automatic tactic with a specific id (which will automatically be prefixed by the project name, e.g. org.eventb.contributors.seqprover). The name attribute is an externalised string used for display purpose. The description attribute is an externalised string that gives the detailed description of the tactic (what it does).

			The <tt>class</tt> attribute must be a valid Java class name which will be used to create an instance of the tactic. This class must implement the <tt>org.eventb.core.seqprover.ITactic</tt> interface.

			For automatic tactics, they must have no input, and most of the time they are just a wrapper around an automatic reasoner. Below is an example of such a tactic.

			public static class AutoTac extends AbsractLazilyConstrTactic {
			@Override
			protected ITactic getSingInstance() {
			return BasicTactics.reasonerTac(new AutoReasoner(), EMPTY_INPUT);
			}
			}

			Here, the implementation extends the abstract class <tt>org.eventb.core.seqprover.eventbExtensions.AutoTactics#AbstractLazilyConstrTactic</tt>. <tt>AutoReasoner</tt> is the name of the class which implements an automatic reasoner expenting an empty input (See [[#Reasoners \| reasoners]]).

			====== Manual Tactics ======
			{{TODO}}

	== Event-B Tactics ==		== Event-B Tactics ==

imported>Pascal: /* General Reasoner */

2010-02-19T10:12:04Z

General Reasoner

← Older revision		Revision as of 10:12, 19 February 2010
Line 260:		Line 260:
	{{TODO}}		{{TODO}}

	==== General ~~Reasoner~~ ====		==== General Reasoners ====
			===== Concepts =====
			If the reasoner does not fall into the above categories, clients need to implement the interface <tt>IReasoner</tt> directly. It includes how to serialize/deserialize the reasoner input. More information to follow ...

			{{TODO}}

			===== Implementation =====
			{{TODO}}

			===== Testing =====
			{{TODO}}

	=== Tactics ===		=== Tactics ===

imported>Pascal: /* Concepts */

2010-02-19T10:10:10Z

Concepts

← Older revision		Revision as of 10:10, 19 February 2010
Line 252:		Line 252:
	The reasoners of this type does not have a single string input (except the sequent) representing the position in the formula (either a hypothesis or the goal) where most appropriate to indicate which inference rule to apply. For example, a reasoner can implement the following inference rules which dealing with conjunction in the hypothesis and in goal.		The reasoners of this type does not have a single string input (except the sequent) representing the position in the formula (either a hypothesis or the goal) where most appropriate to indicate which inference rule to apply. For example, a reasoner can implement the following inference rules which dealing with conjunction in the hypothesis and in goal.

	H, P \|- Q		{{InfRule\|\|<math>\frac{\quad H, P \vdash Q \quad}{H \vdash P \limp Q}</math>}}
	~~-----------------~~
	H \|- P => Q

	===== Implementation =====		===== Implementation =====
	{{TODO}}		{{TODO}}

imported>Pascal: /* Manual Inference */

2010-02-19T10:09:34Z

Manual Inference

@@ Line 248: / Line 248: @@
 {{TODO}}
-==== Manual Inference ====
+==== Manual Inference Reasoners ====
 ==== General Reasoner ====