Event-B - Recent changes [en]

Mode/FT Views

Ilya.lopatkin — Thu, 09 Sep 2010 12:30:44 GMT

←Older revision		Revision as of 12:30, 9 September 2010
Line 174:		Line 174:
	Currently, a static check is performed during a file save operation. This is ok while editing modes, however it will have to be changed: the checks run against a statically checked Event-B models, and changes to the models currently do not trigger the mode views check. If you already have a mode view, and you make changes to the model and want to static-check the view again - please make a slight change to the view (move a mode) and save it. This is a simple solution sufficient at the current stage.		Currently, a static check is performed during a file save operation. This is ok while editing modes, however it will have to be changed: the checks run against a statically checked Event-B models, and changes to the models currently do not trigger the mode views check. If you already have a mode view, and you make changes to the model and want to static-check the view again - please make a slight change to the view (move a mode) and save it. This is a simple solution sufficient at the current stage.
	Saving a mode view also makes a change to the model which triggers the model static check and (if automatic build is enabled) Event-B PO generation. Mode view PO modules are properly integrated into the Rodin builder.		Saving a mode view also makes a change to the model which triggers the model static check and (if automatic build is enabled) Event-B PO generation. Mode view PO modules are properly integrated into the Rodin builder.
		+
		+	== Current issues ==
		+	* No modal SC or POs are performed when one changes the Event-B model retaining the mode view. This is because of SC not being integrated into the Rodin builder. The initial idea is to keep modes outside of the Rodin database, but then we cannot properly hook the Rodin SC tool.
		+	* Copy/paste is not working as one would expect. Pasting adds references to the GMF elements from the source document rather than creating new elements and copying data. This is a default GMF behaviour.
		+	* Mode views might not be seen from the Event-B explorer if a project has been just opened, or a view just created. Please, use the usual eclipse file explorer to open diagrams.

	== References ==		== References ==

Inference Rules

Nicolas — Thu, 09 Sep 2010 12:27:01 GMT

moved datatype rules to extension proof rules page

←Older revision		Revision as of 12:27, 9 September 2010
Line 198:		Line 198:

	{{RRRow}}\| \|\|{{Rulename\|ONE_POINT_R}}\|\|<math>\frac{\textbf{H} \;\;\vdash \;\; {WD}(E) \qquad \textbf{H} \;\;\vdash \;\; \forall x, \ldots, \ldots,z \qdot [y \bcmeq E]\textbf{P} \land \ldots \land \ldots \land [y \bcmeq E]\textbf{Q} \limp [y \bcmeq E]\textbf{R} }{ \textbf{H} \;\;\vdash\;\; \forall x, \ldots, y, \ldots, z \qdot \textbf{P} \land \ldots \land y = E \land \ldots \land \textbf{Q} \limp \textbf{R} }</math>\|\| The rule can be applied with <math>\forall</math> as well as with <math>\exists</math> \|\| A		{{RRRow}}\| \|\|{{Rulename\|ONE_POINT_R}}\|\|<math>\frac{\textbf{H} \;\;\vdash \;\; {WD}(E) \qquad \textbf{H} \;\;\vdash \;\; \forall x, \ldots, \ldots,z \qdot [y \bcmeq E]\textbf{P} \land \ldots \land \ldots \land [y \bcmeq E]\textbf{Q} \limp [y \bcmeq E]\textbf{R} }{ \textbf{H} \;\;\vdash\;\; \forall x, \ldots, y, \ldots, z \qdot \textbf{P} \land \ldots \land y = E \land \ldots \land \textbf{Q} \limp \textbf{R} }</math>\|\| The rule can be applied with <math>\forall</math> as well as with <math>\exists</math> \|\| A
-
-	{{RRRow}}\| \|\|{{Rulename\|DATATYPE_DISTINCT_CASE}}\|\|<math>\frac{\textbf{H}, x=c_1(p_{11}, \ldots, p_{1k}) \;\;\vdash \;\; \textbf{G} \qquad \ldots \qquad \textbf{H}, x=c_n(p_{n1}, \ldots, p_{nl}) \;\;\vdash \;\; \textbf{G} }{ \textbf{H} \;\;\vdash\;\; \textbf{G} }</math>\|\| where <math>x</math> has a datatype <math>DT</math> as type and appears free in <math>\textbf{G}</math>, <math>DT</math> has constructors <math>c_1, \ldots, c_n</math>, parameters <math>p_{ij}</math> are introduced as fresh identifiers \|\| M
-
-	{{RRRow}}\| \|\|{{Rulename\|DATATYPE_INDUCTION}}\|\|<math>\frac{ \textbf{H}, x=c_1(p_1, \ldots, p_k),\textbf{P}(p_{I_1}), \ldots, \textbf{P}(p_{I_l}) \;\;\vdash \;\; \textbf{P}(x) \qquad \ldots \qquad}{ \textbf{H} \;\;\vdash\;\; \textbf{P}(x) }</math>\|\| where <math>x</math> has inductive datatype <math>DT</math> as type and appears free in <math>\textbf{P}</math>; <math>\{p_{I_1}, \ldots, p_{I_l}\} \subseteq \{p_1, \ldots, p_k\}</math> are the inductive parameters (if any); an antecedent is created for every constructor <math>c_i</math> of <math>DT</math>; all parameters are introduced as fresh identifiers; examples [[Datatype Rules\|here]] \|\| M

	\|}		\|}

		+	See also [[Extension Proof Rules#Inference Rules]].

	[[Category:User documentation\|The Proving Perspective]]		[[Category:User documentation\|The Proving Perspective]]
	[[Category:Rodin Platform\|The Proving Perspective]]		[[Category:Rodin Platform\|The Proving Perspective]]
	[[Category:User manual\|The Proving Perspective]]		[[Category:User manual\|The Proving Perspective]]

Extension Proof Rules

Nicolas — Thu, 09 Sep 2010 12:24:56 GMT

copied datatype inference rules

←Older revision		Revision as of 12:24, 9 September 2010
(One intermediate revision not shown.)
Line 2:		Line 2:
	Rules without a <tt>*</tt> are planned to be implemented in future versions.		Rules without a <tt>*</tt> are planned to be implemented in future versions.
	Other conventions used in these tables are described in [[The_Proving_Perspective_%28Rodin_User_Manual%29#Rewrite_Rules]].		Other conventions used in these tables are described in [[The_Proving_Perspective_%28Rodin_User_Manual%29#Rewrite_Rules]].
		+
		+	== Rewrite Rules ==

	{{RRHeader}}		{{RRHeader}}
-	{{RRRow}}\| \|\|{{Rulename\|SIMP_SPECIAL_COND_BTRUE}}\|\|<math> \operatorname{COND}(\btrue, E_1, E_2) \;\;\defi\;\; E_1 </math>\|\| \|\| A	+	{{RRRow}}\|*\|\|{{Rulename\|SIMP_SPECIAL_COND_BTRUE}}\|\|<math> \operatorname{COND}(\btrue, E_1, E_2) \;\;\defi\;\; E_1 </math>\|\| \|\| A
-	{{RRRow}}\| \|\|{{Rulename\|SIMP_SPECIAL_COND_BFALSE}}\|\|<math> \operatorname{COND}(\bfalse, E_1, E_2) \;\;\defi\;\; E_2 </math>\|\| \|\| A	+	{{RRRow}}\|*\|\|{{Rulename\|SIMP_SPECIAL_COND_BFALSE}}\|\|<math> \operatorname{COND}(\bfalse, E_1, E_2) \;\;\defi\;\; E_2 </math>\|\| \|\| A
	\|}		\|}

		+
		+	== Inference Rules ==
		+	{{RRHeader}}
		+	{{RRRow}}\| \|\|{{Rulename\|DATATYPE_DISTINCT_CASE}}\|\|<math>\frac{\textbf{H}, x=c_1(p_{11}, \ldots, p_{1k}) \;\;\vdash \;\; \textbf{G} \qquad \ldots \qquad \textbf{H}, x=c_n(p_{n1}, \ldots, p_{nl}) \;\;\vdash \;\; \textbf{G} }{ \textbf{H} \;\;\vdash\;\; \textbf{G} }</math>\|\| where <math>x</math> has a datatype <math>DT</math> as type and appears free in <math>\textbf{G}</math>, <math>DT</math> has constructors <math>c_1, \ldots, c_n</math>, parameters <math>p_{ij}</math> are introduced as fresh identifiers \|\| M
		+
		+	{{RRRow}}\| \|\|{{Rulename\|DATATYPE_INDUCTION}}\|\|<math>\frac{ \textbf{H}, x=c_1(p_1, \ldots, p_k),\textbf{P}(p_{I_1}), \ldots, \textbf{P}(p_{I_l}) \;\;\vdash \;\; \textbf{P}(x) \qquad \ldots \qquad}{ \textbf{H} \;\;\vdash\;\; \textbf{P}(x) }</math>\|\| where <math>x</math> has inductive datatype <math>DT</math> as type and appears free in <math>\textbf{P}</math>; <math>\{p_{I_1}, \ldots, p_{I_l}\} \subseteq \{p_1, \ldots, p_k\}</math> are the inductive parameters (if any); an antecedent is created for every constructor <math>c_i</math> of <math>DT</math>; all parameters are introduced as fresh identifiers; examples [[Datatype Rules\|here]] \|\| M
		+	\|}

	[[Category:User documentation\|The Proving Perspective]]		[[Category:User documentation\|The Proving Perspective]]
	[[Category:Rodin Platform\|The Proving Perspective]]		[[Category:Rodin Platform\|The Proving Perspective]]
	[[Category:User manual\|The Proving Perspective]]		[[Category:User manual\|The Proving Perspective]]

Special:Log/move

Nicolas — Thu, 09 Sep 2010 10:23:50 GMT

Extension Rewrite Rules moved to Extension Proof Rules: Gathering rewrite and inference rules for extensions in the same page.

Mode/FT Views

Mathieu — Thu, 09 Sep 2010 07:23:05 GMT

add bold

←Older revision		Revision as of 07:23, 9 September 2010
(2 intermediate revisions not shown.)
Line 1:		Line 1:
-	The Mode/FT Views plugin is a modelling environment for constructing modal and fault tolerance features in a concise manner and formally linking them to Event-B models. Fault tolerance part adds additional structural checks and reserves a place to trace FT requirements.	+	The ''Mode/FT Views plugin'' is a modelling environment for constructing modal and fault tolerance features in a concise manner and formally linking them to Event-B models. Fault tolerance part adds additional structural checks and reserves a place to trace FT requirements.

-	A Mode/FT view is a graph diagram containing modes and transitions which provide additional information necessary for establishing a formal connection with the model. The tool statically checks the views and generates a number of proof obligations.	+	A '''Mode/FT view''' is a graph diagram containing modes and transitions which provide additional information necessary for establishing a formal connection with the model. The tool statically checks the views and generates a number of proof obligations.

	== Modes overview ==		== Modes overview ==
Line 50:		Line 50:
	** No transitions can be added which do not project properly onto the abstract transitions. If we project all the concrete modes onto their abstract counterparts, the transitions must either project onto internal transitions within modes or onto mode-to-mode transitions.		** No transitions can be added which do not project properly onto the abstract transitions. If we project all the concrete modes onto their abstract counterparts, the transitions must either project onto internal transitions within modes or onto mode-to-mode transitions.

-	[[Image:Modes_train_refinement4789bng4.png‎\|thumb\|left\| Train drive mode refined]]	+	[[Image:Modes_train_refinement4789bng4.png‎\|thumb\|400px\|left\| Train drive mode refined]]

	To show how this is applied to the train example, let us refine one of the modes (''drive'') into three new modes ''auto_drive'', ''manual_drive'', and ''emergency_stop'' and add appropriate transitions. There can be any transitions between these three modes since they all represent internal behaviour in the mode ''drive''. However, now we see two transitions which both lead to the ''stopped'' mode (''emrg_stop'' and ''stop'') - these initiate from different concrete modes but both refine the same abstract transition and are therefore valid. Note that we are not allowed to add transitions initiating from the ''stopped'' mode and leading to one of the new ''drive'' modes (and thus bypassing the ''doors_closing'' mode) - this would violate the abstract mode diagram since such transition didn't exist on the previous level.		To show how this is applied to the train example, let us refine one of the modes (''drive'') into three new modes ''auto_drive'', ''manual_drive'', and ''emergency_stop'' and add appropriate transitions. There can be any transitions between these three modes since they all represent internal behaviour in the mode ''drive''. However, now we see two transitions which both lead to the ''stopped'' mode (''emrg_stop'' and ''stop'') - these initiate from different concrete modes but both refine the same abstract transition and are therefore valid. Note that we are not allowed to add transitions initiating from the ''stopped'' mode and leading to one of the new ''drive'' modes (and thus bypassing the ''doors_closing'' mode) - this would violate the abstract mode diagram since such transition didn't exist on the previous level.
Line 132:		Line 132:
	The FT elements that can be added to the modal diagrams include two types of transition specialisation - '''''error''''' and '''''recovery'''''. An error always originates in a ''normal'' mode and leads to switching to a ''degraded'' or a ''recovery mode''. A recovery transition switches back from the recovery mode to the normal one. Note that mode attribution to the specific type is relative and is not regulated by the tool. It is a design choice of which modes to be considered normal and which degraded/recovery.		The FT elements that can be added to the modal diagrams include two types of transition specialisation - '''''error''''' and '''''recovery'''''. An error always originates in a ''normal'' mode and leads to switching to a ''degraded'' or a ''recovery mode''. A recovery transition switches back from the recovery mode to the normal one. Note that mode attribution to the specific type is relative and is not regulated by the tool. It is a design choice of which modes to be considered normal and which degraded/recovery.

-	[[Image:Modes_train_ft5959588.png‎\|thumb\| Emergency stop is now a recovery mode which is triggerd by (red) error transitions]]	+	[[Image:Modes_train_ft5959588.png‎\|thumb\|400px\| Emergency stop is now a recovery mode which is triggerd by (red) error transitions]]

	There are additional structural checks which the tool performs over the FT transitions:		There are additional structural checks which the tool performs over the FT transitions:

Extending the Proof Obligation Generator(How to extend Rodin Tutorial)

Pascal — Wed, 08 Sep 2010 14:42:55 GMT

Step 3: Removing a PO:

(Difference between revisions)

Mode/FT Views

Ilya.lopatkin — Tue, 07 Sep 2010 17:05:14 GMT

(Difference between revisions)

Extending the Proof Obligation Generator(How to extend Rodin Tutorial)

Pascal — Tue, 07 Sep 2010 16:19:53 GMT

Step 1 : Adding POG modules:

←Older revision		Revision as of 16:19, 7 September 2010
(4 intermediate revisions not shown.)
Line 3:		Line 3:
	=== In this part ===		=== In this part ===

-	We will see how to create proof obligations ~~to discharge~~ for the machines relatively to our extensions for Probabilistic Reasoning and after having statically checked ~~the~~ machines. The latter operation is the first part of the proof obligation generation as the proof obligation generator takes statically checked files in input. One will notice that the provided architecture for static checking is really similar to the one for proof obligation generation. Thus, it can be useful for the reader to understand well the previous part of this tutorial, as we will not repeat all the ideas shared by the both processes.	+	We will see how to create proof obligations (PO) for the machines relatively to our extensions for Probabilistic Reasoning and after having statically checked these machines. The latter operation is the first part of the proof obligation generation as the proof obligation generator (POG) takes statically checked files as input. One will notice that the provided architecture for static checking is really similar to the one for proof obligation generation. Thus, it can be useful for the reader to understand well the previous part of this tutorial, as we will not repeat all the ideas shared by the both processes.
-	The question here is "'''What needs to be mathematically proved with ~~those~~ newly added elements in hands?'''".	+	The question here is "'''What needs to be mathematically proved with these newly added elements in hands?'''".
		+
		+	We will study here the case of the ''BFN'' proof obligation, which is described in the paper. This PO overrides the ''FIN'' PO. Thus, we will see in this section how to:
		+	* Remove the ''FIN'' PO, which is generated by default.
		+	* Add our new ''BFN'' PO.

-	~~We will study here, the case of the ''BFN'' proof obligation, which is described in the paper. This PO overrides the FIN proof obligation. Thus we will see here, how to :~~
-	* remove the FIN PO which is generated by default,
-	* add our new ''BFN'' PO.
-
	=== Principles ===		=== Principles ===
		+	1. To extend the POG in order to add some POs that have to be discharged, '''define a proof obligation processor module''' using the extension point <tt>org.eventb.core.pogModuleTypes</tt>.<br>
		+	2. Then, '''set up a configuration''' involving these modules and giving them a hierarchy. This is done exactly the same way as for creating a static checker configuration.<br>
		+	3. Finally, '''add this POG configuration''' to the default one, so the proof obligation generation can be performed.<br>

-	1. To extend the proof obligation generator (POG) in order to add some proof obligations that one has to discharge, one has to '''define a proof obligation processor module''' using the extension point : <tt>org.eventb.core.pogModuleTypes</tt>.<br>	+	We will here show how to generate one PO. We will add the PO named ''BFN'' to ensure that the Bound is a natural number or is finite. It will be generated once for all for the machine taken into account. Moreover, this PO overrides the default ''FIN'' PO which is generated if a convergent event (with the associated variant) is present in the model. If a probabilistic event is in the machine, we want to create our ''BFN'' PO, thus we have to remove the ''FIN'' PO.
-	~~2. Then , one has to '''set up a configuration''' involving those modules and giving them a hierachy. This is done exactly the same way as for creating a static checker configuration.<br>~~	+
-	~~3. Finally, it is needed to '''add this POG configuration''' to the default one, so the proof obligation generation can be performed.<br>~~	+
-		+
-		+
-	We ~~want~~ here to show how to generate one ~~proof obligation~~. We will add the PO named ''BFN'' to ensure that the ~~bound~~ is a natural number or finite. It will be generated once for all for the machine taken into account. Moreover, this PO overrides the default FIN ~~proof obligation~~ which is generated if a convergent event (with the associated variant) is present in the model. If a probabilistic event is in the machine, we want to create our ''BFN'' PO, thus we have to remove the FIN PO.	+

-	In step 1, we will explain how to create our PO ''BFN'' using ~~informations~~ in the state repository ~~that~~ we will add in step 2, so in step 3 we ~~could~~ create a filter to remove the PO ''FIN'' if our machine contains a probabilistic event.	+	In step 1, we will explain how to create our ''BFN'' PO using information in the state repository, we will add it in step 2, and then in step 3 we will create a filter to remove the ''FIN'' PO if our machine contains a probabilistic event.

-	=== Step 1 : Adding POG modules ===	+	=== Step 1: Adding POG modules ===

-	As we know that the POG takes its input from the static checker, the presence of a statically checked ~~bound~~ (ISCBound) in the statically checked model, means that one aims to prove the probabilistic convergence of this model. Thus, this information shall be shared ~~throught~~ our ~~hierachy~~ of POG modules, as it triggers the operations they could perform.	+	As we know that the POG takes its input from the static checker output, the presence of a statically checked Bound element (<tt>ISCBound</tt>) in the statically checked model means that one aims to prove the probabilistic convergence of this model. Thus, this information shall be shared through our hierarchy of POG modules, as it triggers the operations that they could perform.

	We will anticipate using this information (stored in a <tt>IPOGState</tt>) to create the ''BFN'' proof obligation :		We will anticipate using this information (stored in a <tt>IPOGState</tt>) to create the ''BFN'' proof obligation :

Special:Log/upload

Ilya.lopatkin — Tue, 07 Sep 2010 14:43:48 GMT

uploaded "Image:Modes train ft5959588.png": The train mode view with an emergency stop recovery mode

Special:Log/upload

Ilya.lopatkin — Tue, 07 Sep 2010 13:48:39 GMT

uploaded "Image:Modes editing tips 45978567.png": The mode view editor

Datatype Rules

Nicolas — Tue, 07 Sep 2010 13:37:11 GMT

Datatypes used:

←Older revision		Revision as of 13:37, 7 September 2010
(2 intermediate revisions not shown.)
Line 37:		Line 37:

	Let us have a function		Let us have a function
-	<math>\operatorname{height} \in \operatorname{Tree} \tfun \N</math> defining the height of a tree	+	<math>\operatorname{height} \in \operatorname{Tree} \tfun \N</math>
		+	defining the height of a tree

	== Distinct Case ==		== Distinct Case ==
Line 46:		Line 47:


-	=== ~~Application to~~ directions ===	+	=== Distinct Case on directions ===


Line 55:		Line 56:

	The resulting proof step is		The resulting proof step is
-	<math>\frac{ d=\operatorname{north} \;\vdash \; \operatorname{move}(x \mapsto y \mapsto ~~\operatorname{north}~~) \neq x \mapsto y \qquad d=\operatorname{east} \;\vdash \; \operatorname{move}(x \mapsto y \mapsto ~~\operatorname{east}~~) \neq x \mapsto y \qquad d=\operatorname{south} \;\vdash \; \operatorname{move}(x \mapsto y \mapsto ~~\operatorname{south}~~) \neq x \mapsto y \qquad d=\operatorname{west} \;\vdash \; \operatorname{move}(x \mapsto y \mapsto ~~\operatorname{west}~~) \neq x \mapsto y }{ \;\;\vdash\;\; \operatorname{move}(x \mapsto y \mapsto d) \neq x \mapsto y }</math>	+	<math>\frac{ d=\operatorname{north} \;\vdash \; \operatorname{move}(x \mapsto y \mapsto d) \neq x \mapsto y \qquad d=\operatorname{east} \;\vdash \; \operatorname{move}(x \mapsto y \mapsto d) \neq x \mapsto y \qquad d=\operatorname{south} \;\vdash \; \operatorname{move}(x \mapsto y \mapsto d) \neq x \mapsto y \qquad d=\operatorname{west} \;\vdash \; \operatorname{move}(x \mapsto y \mapsto d) \neq x \mapsto y }{ \;\;\vdash\;\; \operatorname{move}(x \mapsto y \mapsto d) \neq x \mapsto y }</math>

	further simplifications depend on the existence of rules about move and the various directions.		further simplifications depend on the existence of rules about move and the various directions.

-	=== ~~Application to~~ lists ===	+	=== Distinct Case on lists ===

	Starting from goal		Starting from goal
Line 67:		Line 68:
	we can free variable l then apply Distinct Case on it:		we can free variable l then apply Distinct Case on it:

-	<math>\frac{ l=\operatorname{nil} \;\vdash \; \exists x \qdot \operatorname{member}(x,~~\operatorname{nil}~~) \land (\forall y \qdot \operatorname{member}(y,~~\operatorname{nil}~~) \limp y \leq x) \qquad l=\operatorname{cons}(head0, tail1) \;\vdash \; \exists x \qdot \operatorname{member}(x,~~\operatorname{cons}(head0, tail1)~~) \land (\forall y \qdot \operatorname{member}(y,~~\operatorname{cons}(head0, tail1)~~) \limp y \leq x) }{ \;\;\vdash\;\; \exists x \qdot \operatorname{member}(x,l) \land (\forall y \qdot \operatorname{member}(y,l) \limp y \leq x) }</math>	+	<math>\frac{ l=\operatorname{nil} \;\vdash \; \exists x \qdot \operatorname{member}(x,l) \land (\forall y \qdot \operatorname{member}(y,l) \limp y \leq x) \qquad l=\operatorname{cons}(head0, tail1) \;\vdash \; \exists x \qdot \operatorname{member}(x,l) \land (\forall y \qdot \operatorname{member}(y,l) \limp y \leq x) }{ \;\;\vdash\;\; \exists x \qdot \operatorname{member}(x,l) \land (\forall y \qdot \operatorname{member}(y,l) \limp y \leq x) }</math>

-	The left antecedent shows that the case of the nil list has been forgotten when writing the theorem.	+	The left antecedent shows that the case of the nil list has been forgotten when writing the theorem. The right antecedent looks as hard to prove as the initial goal (but see [[#Induction on lists\|the induction application]]).

-	=== ~~Application to~~ trees ===	+	=== Distinct Case on trees ===

	Starting from goal		Starting from goal
Line 79:		Line 80:
	we can free variables l,v,r,t then apply IMP_R and then Distinct Case on t:		we can free variables l,v,r,t then apply IMP_R and then Distinct Case on t:

-	<math>\frac{ t = \operatorname{node}(l,v,r) \;,\;\; t=\operatorname{empty} \;\vdash \; \operatorname{height}(l) < \operatorname{height}(~~\operatorname{empty}~~) \qquad t = \operatorname{node}(l,v,r) \;,\;\; t = \operatorname{node}(\operatorname{left0},\operatorname{value1},\operatorname{right2}) \;\vdash \; \operatorname{height}(l) < \operatorname{height}(~~\operatorname{node}(\operatorname{left0},\operatorname{value1},\operatorname{right2})~~) }{ t = \operatorname{node}(l,v,r) \;\;\vdash\;\; \operatorname{height}(l) < \operatorname{height}(t) }</math>	+	<math>\frac{ t = \operatorname{node}(l,v,r) \;,\;\; t=\operatorname{empty} \;\vdash \; \operatorname{height}(l) < \operatorname{height}(t) \qquad t = \operatorname{node}(l,v,r) \;,\;\; t = \operatorname{node}(\operatorname{left0},\operatorname{value1},\operatorname{right2}) \;\vdash \; \operatorname{height}(l) < \operatorname{height}(t) }{ t = \operatorname{node}(l,v,r) \;\;\vdash\;\; \operatorname{height}(l) < \operatorname{height}(t) }</math>

	the left antecedent will then be proved using the contradiction in hypotheses. The right one will require eh on t in hypotheses and SIMP_EQUAL_CONSTR, then properties about height.		the left antecedent will then be proved using the contradiction in hypotheses. The right one will require eh on t in hypotheses and SIMP_EQUAL_CONSTR, then properties about height.
Line 85:		Line 86:
	== Induction ==		== Induction ==

-	{{~~TODO~~}}	+	The rule states
		+
		+	<math>\frac{ \textbf{H}, x=c_1(p_1, \ldots, p_k),\textbf{P}(p_{I_1}), \ldots, \textbf{P}(p_{I_l}) \;\;\vdash \;\; \textbf{P}(x) \qquad \ldots \qquad}{ \textbf{H} \;\;\vdash\;\; \textbf{P}(x) }</math>
		+
		+	The only difference with Distinct Case resides in the <math>\textbf{P}(p_{I_1}), \ldots, \textbf{P}(p_{I_l})</math> hypotheses for inductive parameters.
		+
		+	=== Induction on directions ===
		+
		+
		+	Starting from goal
		+	<math>\forall x,y,d \qdot \operatorname{move}(x \mapsto y \mapsto d) \neq x \mapsto y</math>
		+
		+	we can free variables x,y,d then apply Induction on d:
		+
		+	The resulting proof step is
		+	<math>\frac{ d=\operatorname{north} \;\vdash \; \operatorname{move}(x \mapsto y \mapsto d) \neq x \mapsto y \qquad d=\operatorname{east} \;\vdash \; \operatorname{move}(x \mapsto y \mapsto d) \neq x \mapsto y \qquad d=\operatorname{south} \;\vdash \; \operatorname{move}(x \mapsto y \mapsto d) \neq x \mapsto y \qquad d=\operatorname{west} \;\vdash \; \operatorname{move}(x \mapsto y \mapsto d) \neq x \mapsto y }{ \;\;\vdash\;\; \operatorname{move}(x \mapsto y \mapsto d) \neq x \mapsto y }</math>
		+
		+	As we can see, it is exactly the same proof step as for Distinct Case: the reason is that the direction constructors contain no parameters, a fortiori no inductive parameters, so there are no additional hypotheses.
		+
		+	=== Induction on lists ===
		+
		+	Starting from goal
		+
		+	<math>\forall l \qdot \exists x \qdot \operatorname{member}(x,l) \land (\forall y \qdot \operatorname{member}(y,l) \limp y \leq x)</math>
		+
		+	we can free variable l then apply Induction on it:
		+
		+	<math>\frac{ l=\operatorname{nil} \;\vdash \; \exists x \qdot \operatorname{member}(x,l) \land (\forall y \qdot \operatorname{member}(y,l) \limp y \leq x) \qquad l=\operatorname{cons}(head0, tail1) \;,\; \exists x \qdot \operatorname{member}(x,tail1) \land (\forall y \qdot \operatorname{member}(y,tail1) \limp y \leq x) \;\vdash \; \exists x \qdot \operatorname{member}(x,l) \land (\forall y \qdot \operatorname{member}(y,l) \limp y \leq x) }{ \;\;\vdash\;\; \exists x \qdot \operatorname{member}(x,l) \land (\forall y \qdot \operatorname{member}(y,l) \limp y \leq x) }</math>
		+
		+	The left antecedent shows the same problem as Distinct for nil list. The benefit of the Induction is in the right antecedent with the additional hypothesis that the predicate stands for tail1. Next step will be to make eh on l, free the x in the tail1 hypothesis, then use it to instantiate the x in the goal with <math>\operatorname{max}(\operatorname{head0}, x_{\operatorname{tail1}})</math>.
		+	In this proof, application of Distinct Case does not allow to complete the proof (at least not so easily), whereas Induction does.
		+
		+	=== Induction on trees ===
		+
		+	Starting from goal
		+
		+	<math>\forall l,v,r,t \qdot t = \operatorname{node}(l,v,r) \limp \operatorname{height}(l) < \operatorname{height}(t)</math>
		+
		+	we can free variables l,v,r,t then apply IMP_R and then Induction on t:
		+
		+	<math>\frac{ t = \operatorname{node}(l,v,r) \;,\;\; t=\operatorname{empty} \;\vdash \; \operatorname{height}(l) < \operatorname{height}(\operatorname{empty}) \qquad t = \operatorname{node}(l,v,r) \;,\;\; t = \operatorname{node}(\operatorname{left0},\operatorname{value1},\operatorname{right2}) \;,\;\; \operatorname{height}(\operatorname{left0}) < \operatorname{height}(t) \;,\;\; \operatorname{height}(\operatorname{right2}) < \operatorname{height}(t) \;\vdash \; \operatorname{height}(l) < \operatorname{height}(\operatorname{node}(\operatorname{left0},\operatorname{value1},\operatorname{right2})) }{ t = \operatorname{node}(l,v,r) \;\;\vdash\;\; \operatorname{height}(l) < \operatorname{height}(t) }</math>
		+
		+	the left antecedent will then be proved using the contradiction in hypotheses. In the right one, additional induction hypotheses do not provide much help: in this situation, using Distinct Case and properties about height is sufficient to discharge the proof.

Extending the Static Checker (How to extend Rodin Tutorial)

Pascal — Tue, 07 Sep 2010 07:29:31 GMT

←Older revision		Revision as of 07:29, 7 September 2010
(3 intermediate revisions not shown.)
Line 1:		Line 1:
-	{{Navigation\|Previous= [[~~Extending_the_Static_Checker~~(How_to_extend_Rodin_Tutorial)]] \| Up= [[Plug-in_Tutorial\|How to extend Rodin Tutorial (Index)]] \| Next= }}	+	{{Navigation\|Previous= [[Providing_help_for_your_plug-in_(How_to_extend_Rodin_Tutorial) \| Providing help]] \| Up= [[Plug-in_Tutorial\|How to extend Rodin Tutorial (Index)]] \| Next= [[Extending_the_Proof_Obligation_Generator(How_to_extend_Rodin_Tutorial) \| Generating the proof obligations]]}}

	=== In this part ===		=== In this part ===
Line 257:		Line 257:
	}		}

-		+	{{Navigation\|Previous= [[Providing_help_for_your_plug-in_(How_to_extend_Rodin_Tutorial) \| Providing help]] \| Up= [[Plug-in_Tutorial\|How to extend Rodin Tutorial (Index)]] \| Next= [[Extending_the_Proof_Obligation_Generator(How_to_extend_Rodin_Tutorial) \| Generating the proof obligations]]}}
-	{{Navigation\|Previous= [[~~Extending_the_Static_Checker~~(How_to_extend_Rodin_Tutorial)]] \| Up= [[Plug-in_Tutorial\|How to extend Rodin Tutorial (Index)]] \| Next= }}	+

	[[Category:Developer documentation\|*Index]]		[[Category:Developer documentation\|*Index]]
	[[Category:Rodin Platform\|*Index]]		[[Category:Rodin Platform\|*Index]]
	[[Category:Tutorial\|*Index]]		[[Category:Tutorial\|*Index]]

Extending the Proof Obligation Generator(How to extend Rodin Tutorial)

Pascal — Tue, 07 Sep 2010 07:23:56 GMT

(Difference between revisions)

Special:Log/move

Pascal — Tue, 07 Sep 2010 07:19:52 GMT

Extending the Proof Obligation Generator(How to extend Rodin Tutorial) moved to Extending the Proof Obligation Generator (How to extend Rodin Tutorial)

Providing help for your plug-in (How to extend Rodin Tutorial)

Pascal — Tue, 07 Sep 2010 07:18:00 GMT

←Older revision		Revision as of 07:18, 7 September 2010
Line 1:		Line 1:
-	{{Navigation\|Previous= [[Extending_Rodin_Pretty_Print_Page(How_to_extend_Rodin_Tutorial)\|Displaying added elements in the Pretty Print Page]]\|Next=[[~~'''FIXME'''~~\|Extending the ~~structured editor~~]] \| Up= [[Plug-in_Tutorial\|How to extend Rodin Tutorial (Index)]]}}	+	{{Navigation\|Previous= [[Extending_Rodin_Pretty_Print_Page(How_to_extend_Rodin_Tutorial)\|Displaying added elements in the Pretty Print Page]]\|Next=[[Extending_the_Static_Checker(How_to_extend_Rodin_Tutorial)\|Extending the static checker]] \| Up= [[Plug-in_Tutorial\|How to extend Rodin Tutorial (Index)]]}}

	=== Creating the Help Plug-in ===		=== Creating the Help Plug-in ===
Line 61:		Line 61:
	[[Image:wiki2help.png]]		[[Image:wiki2help.png]]

-	{{Navigation\|Previous= [[Extending_Rodin_Pretty_Print_Page(How_to_extend_Rodin_Tutorial)\|Displaying added elements in the Pretty Print Page]]\|Next= [[~~'''FIXME'''~~\|Extending the ~~structured editor~~]] \| Up= [[Plug-in_Tutorial\|How to extend Rodin Tutorial (Index)]]}}	+	{{Navigation\|Previous= [[Extending_Rodin_Pretty_Print_Page(How_to_extend_Rodin_Tutorial)\|Displaying added elements in the Pretty Print Page]]\|Next=[[Extending_the_Static_Checker(How_to_extend_Rodin_Tutorial)\|Extending the static checker]] \| Up= [[Plug-in_Tutorial\|How to extend Rodin Tutorial (Index)]]}}

	[[Category:Developer documentation\|*Index]]		[[Category:Developer documentation\|*Index]]
	[[Category:Rodin Platform\|*Index]]		[[Category:Rodin Platform\|*Index]]
	[[Category:Tutorial\|*Index]]		[[Category:Tutorial\|*Index]]

Special:Log/move

Pascal — Tue, 07 Sep 2010 07:17:12 GMT

Extending the Static Checker(How to extend Rodin Tutorial) moved to Extending the Static Checker (How to extend Rodin Tutorial)

Providing help for your plug-in (How to extend Rodin Tutorial)

Pascal — Tue, 07 Sep 2010 07:16:36 GMT

←Older revision		Revision as of 07:16, 7 September 2010
Line 1:		Line 1:
-	{{Navigation\|Previous= [[Extending_Rodin_Pretty_Print_Page(How_to_extend_Rodin_Tutorial)\|~~Display~~ added elements in the Pretty Print Page]]\|Next=[['''FIXME'''\|Extending the structured editor]] \| Up= [[Plug-in_Tutorial\|How to extend Rodin Tutorial (Index)]]}}	+	{{Navigation\|Previous= [[Extending_Rodin_Pretty_Print_Page(How_to_extend_Rodin_Tutorial)\|Displaying added elements in the Pretty Print Page]]\|Next=[['''FIXME'''\|Extending the structured editor]] \| Up= [[Plug-in_Tutorial\|How to extend Rodin Tutorial (Index)]]}}

	=== Creating the Help Plug-in ===		=== Creating the Help Plug-in ===
Line 61:		Line 61:
	[[Image:wiki2help.png]]		[[Image:wiki2help.png]]

-	{{Navigation\|Previous= [[~~'''FIXME'''~~\|~~Extending~~ the ~~Proof Obligation Generator~~]]\|Next= [['''FIXME'''\|Extending the structured editor]] \| Up= [[Plug-in_Tutorial\|How to extend Rodin Tutorial (Index)]]}}	+	{{Navigation\|Previous= [[Extending_Rodin_Pretty_Print_Page(How_to_extend_Rodin_Tutorial)\|Displaying added elements in the Pretty Print Page]]\|Next= [['''FIXME'''\|Extending the structured editor]] \| Up= [[Plug-in_Tutorial\|How to extend Rodin Tutorial (Index)]]}}

	[[Category:Developer documentation\|*Index]]		[[Category:Developer documentation\|*Index]]
	[[Category:Rodin Platform\|*Index]]		[[Category:Rodin Platform\|*Index]]
	[[Category:Tutorial\|*Index]]		[[Category:Tutorial\|*Index]]

Extending the Rodin Event-B Explorer (How to extend Rodin Tutorial)

Pascal — Tue, 07 Sep 2010 07:15:20 GMT

←Older revision		Revision as of 07:15, 7 September 2010
Line 1:		Line 1:
-	{{Navigation\|Previous= [[Extending_the_Rodin_Structured_Editor_(How_to_extend_Rodin_Tutorial)\|Extending the Rodin Structured Editor]]\| Next=[[Extending_Rodin_Pretty_Print_Page(How_to_extend_Rodin_Tutorial)\|~~Display~~ added elements in the Pretty Print Page]] \| Up= [[Plug-in_Tutorial\|How to extend Rodin Tutorial (Index)]]}}	+	{{Navigation\|Previous= [[Extending_the_Rodin_Structured_Editor_(How_to_extend_Rodin_Tutorial)\|Extending the Rodin Structured Editor]]\| Next=[[Extending_Rodin_Pretty_Print_Page(How_to_extend_Rodin_Tutorial)\|Displaying added elements in the Pretty Print Page]] \| Up= [[Plug-in_Tutorial\|How to extend Rodin Tutorial (Index)]]}}

	=== In this part ===		=== In this part ===
Line 149:		Line 149:
	That's all! You are now able to view ''Bound'' elements in the Event-B Explorer view.		That's all! You are now able to view ''Bound'' elements in the Event-B Explorer view.

-	{{Navigation\|Previous= [[Extending_the_Rodin_Structured_Editor_(How_to_extend_Rodin_Tutorial)\|Extending the Rodin Structured Editor]]\| Next=[[Extending_Rodin_Pretty_Print_Page(How_to_extend_Rodin_Tutorial)\|~~Display~~ added elements in the Pretty Print Page]] \| Up= [[Plug-in_Tutorial\|How to extend Rodin Tutorial (Index)]]}}	+	{{Navigation\|Previous= [[Extending_the_Rodin_Structured_Editor_(How_to_extend_Rodin_Tutorial)\|Extending the Rodin Structured Editor]]\| Next=[[Extending_Rodin_Pretty_Print_Page(How_to_extend_Rodin_Tutorial)\|Displaying added elements in the Pretty Print Page]] \| Up= [[Plug-in_Tutorial\|How to extend Rodin Tutorial (Index)]]}}

	[[Category:Developer documentation\|*Index]]		[[Category:Developer documentation\|*Index]]
	[[Category:Rodin Platform\|*Index]]		[[Category:Rodin Platform\|*Index]]
	[[Category:Tutorial\|*Index]]		[[Category:Tutorial\|*Index]]

Extending the Rodin database (How to extend Rodin Tutorial)

Pascal — Tue, 07 Sep 2010 07:14:27 GMT

←Older revision		Revision as of 07:14, 7 September 2010
Line 120:		Line 120:
	As we had a detailed view (captures) of all the actions further needed, the next parts of this tutorial will focus only on the extensions.		As we had a detailed view (captures) of all the actions further needed, the next parts of this tutorial will focus only on the extensions.

-	{{Navigation\|Previous= [[Creating_a_new_plug-in_using_eclipse_(How_to_extend_Rodin_Tutorial)\|Creating our plug-in]]\|Next= [[Extend_Rodin_Structured_Editor_(How_to_extend_Rodin_Tutorial)\|~~Extend~~ the structured editor]] \| Up= [[Plug-in_Tutorial\|How to extend Rodin Tutorial (Index)]]}}	+	{{Navigation\|Previous= [[Creating_a_new_plug-in_using_eclipse_(How_to_extend_Rodin_Tutorial)\|Creating our plug-in]]\|Next= [[Extend_Rodin_Structured_Editor_(How_to_extend_Rodin_Tutorial)\|Extending the structured editor]] \| Up= [[Plug-in_Tutorial\|How to extend Rodin Tutorial (Index)]]}}

	[[Category:Developer documentation\|*Index]]		[[Category:Developer documentation\|*Index]]
	[[Category:Rodin Platform\|*Index]]		[[Category:Rodin Platform\|*Index]]
	[[Category:Tutorial\|*Index]]		[[Category:Tutorial\|*Index]]

Datatype Rules

Nicolas — Mon, 06 Sep 2010 17:43:35 GMT

Application to trees:

←Older revision		Revision as of 17:43, 6 September 2010
(4 intermediate revisions not shown.)
Line 52:		Line 52:
	<math>\forall x,y,d \qdot \operatorname{move}(x \mapsto y \mapsto d) \neq x \mapsto y</math>		<math>\forall x,y,d \qdot \operatorname{move}(x \mapsto y \mapsto d) \neq x \mapsto y</math>

-	we can free variables x,y,d then apply Distinct Case:	+	we can free variables x,y,d then apply Distinct Case on d:

	The resulting proof step is		The resulting proof step is
-	<math>\frac{ d=\operatorname{north} \;\vdash \; \operatorname{move}(x \mapsto y \mapsto \operatorname{north}) \neq x \mapsto y \qquad d=east \;\vdash \; \operatorname{move}(x \mapsto y \mapsto \operatorname{east}) \neq x \mapsto y \qquad d=south \;\vdash \; \operatorname{move}(x \mapsto y \mapsto \operatorname{south}) \neq x \mapsto y \qquad d=west \;\vdash \; \operatorname{move}(x \mapsto y \mapsto \operatorname{west}) \neq x \mapsto y }{ \;\;\vdash\;\; \operatorname{move}(x \mapsto y \mapsto d) \neq x \mapsto y }</math>	+	<math>\frac{ d=\operatorname{north} \;\vdash \; \operatorname{move}(x \mapsto y \mapsto \operatorname{north}) \neq x \mapsto y \qquad d=\operatorname{east} \;\vdash \; \operatorname{move}(x \mapsto y \mapsto \operatorname{east}) \neq x \mapsto y \qquad d=\operatorname{south} \;\vdash \; \operatorname{move}(x \mapsto y \mapsto \operatorname{south}) \neq x \mapsto y \qquad d=\operatorname{west} \;\vdash \; \operatorname{move}(x \mapsto y \mapsto \operatorname{west}) \neq x \mapsto y }{ \;\;\vdash\;\; \operatorname{move}(x \mapsto y \mapsto d) \neq x \mapsto y }</math>

	further simplifications depend on the existence of rules about move and the various directions.		further simplifications depend on the existence of rules about move and the various directions.
Line 61:		Line 61:
	=== Application to lists ===		=== Application to lists ===

-	~~{{TODO}}~~	+	Starting from goal

-	!l ~~oftype list(~~\~~Z). #~~x. member(x,l) & (!y. member(y,l) => y <= x)	+	<math>\forall l \qdot \exists x \qdot \operatorname{member}(x,l) \land (\forall y \qdot \operatorname{member}(y,l) \limp y \leq x)</math>

-	~~evidence~~ that nil list has been forgotten in the ~~predicate~~	+	we can free variable l then apply Distinct Case on it:
		+
		+	<math>\frac{ l=\operatorname{nil} \;\vdash \; \exists x \qdot \operatorname{member}(x,\operatorname{nil}) \land (\forall y \qdot \operatorname{member}(y,\operatorname{nil}) \limp y \leq x) \qquad l=\operatorname{cons}(head0, tail1) \;\vdash \; \exists x \qdot \operatorname{member}(x,\operatorname{cons}(head0, tail1)) \land (\forall y \qdot \operatorname{member}(y,\operatorname{cons}(head0, tail1)) \limp y \leq x) }{ \;\;\vdash\;\; \exists x \qdot \operatorname{member}(x,l) \land (\forall y \qdot \operatorname{member}(y,l) \limp y \leq x) }</math>
		+
		+	The left antecedent shows that the case of the nil list has been forgotten when writing the theorem.

	=== Application to trees ===		=== Application to trees ===

-	{{~~TODO~~}}	+	Starting from goal
		+
		+	<math>\forall l,v,r,t \qdot t = \operatorname{node}(l,v,r) \limp \operatorname{height}(l) < \operatorname{height}(t)</math>
		+
		+	we can free variables l,v,r,t then apply IMP_R and then Distinct Case on t:
		+
		+	<math>\frac{ t = \operatorname{node}(l,v,r) \;,\;\; t=\operatorname{empty} \;\vdash \; \operatorname{height}(l) < \operatorname{height}(\operatorname{empty}) \qquad t = \operatorname{node}(l,v,r) \;,\;\; t = \operatorname{node}(\operatorname{left0},\operatorname{value1},\operatorname{right2}) \;\vdash \; \operatorname{height}(l) < \operatorname{height}(\operatorname{node}(\operatorname{left0},\operatorname{value1},\operatorname{right2})) }{ t = \operatorname{node}(l,v,r) \;\;\vdash\;\; \operatorname{height}(l) < \operatorname{height}(t) }</math>

-	~~!l,v,r~~. t ~~= node(l~~,~~v,r) =>~~ height~~(l) < height(t)~~	+	the left antecedent will then be proved using the contradiction in hypotheses. The right one will require eh on t in hypotheses and SIMP_EQUAL_CONSTR, then properties about height.

	== Induction ==		== Induction ==

	{{TODO}}		{{TODO}}

←Older revision		Revision as of 12:27, 9 September 2010
Line 198:		Line 198:

	{{RRRow}}\| \|\|{{Rulename\|ONE_POINT_R}}\|\|<math>\frac{\textbf{H} \;\;\vdash \;\; {WD}(E) \qquad \textbf{H} \;\;\vdash \;\; \forall x, \ldots, \ldots,z \qdot [y \bcmeq E]\textbf{P} \land \ldots \land \ldots \land [y \bcmeq E]\textbf{Q} \limp [y \bcmeq E]\textbf{R} }{ \textbf{H} \;\;\vdash\;\; \forall x, \ldots, y, \ldots, z \qdot \textbf{P} \land \ldots \land y = E \land \ldots \land \textbf{Q} \limp \textbf{R} }</math>\|\| The rule can be applied with <math>\forall</math> as well as with <math>\exists</math> \|\| A		{{RRRow}}\| \|\|{{Rulename\|ONE_POINT_R}}\|\|<math>\frac{\textbf{H} \;\;\vdash \;\; {WD}(E) \qquad \textbf{H} \;\;\vdash \;\; \forall x, \ldots, \ldots,z \qdot [y \bcmeq E]\textbf{P} \land \ldots \land \ldots \land [y \bcmeq E]\textbf{Q} \limp [y \bcmeq E]\textbf{R} }{ \textbf{H} \;\;\vdash\;\; \forall x, \ldots, y, \ldots, z \qdot \textbf{P} \land \ldots \land y = E \land \ldots \land \textbf{Q} \limp \textbf{R} }</math>\|\| The rule can be applied with <math>\forall</math> as well as with <math>\exists</math> \|\| A
-
-	{{RRRow}}\| \|\|{{Rulename\|DATATYPE_DISTINCT_CASE}}\|\|<math>\frac{\textbf{H}, x=c_1(p_{11}, \ldots, p_{1k}) \;\;\vdash \;\; \textbf{G} \qquad \ldots \qquad \textbf{H}, x=c_n(p_{n1}, \ldots, p_{nl}) \;\;\vdash \;\; \textbf{G} }{ \textbf{H} \;\;\vdash\;\; \textbf{G} }</math>\|\| where <math>x</math> has a datatype <math>DT</math> as type and appears free in <math>\textbf{G}</math>, <math>DT</math> has constructors <math>c_1, \ldots, c_n</math>, parameters <math>p_{ij}</math> are introduced as fresh identifiers \|\| M
-
-	{{RRRow}}\| \|\|{{Rulename\|DATATYPE_INDUCTION}}\|\|<math>\frac{ \textbf{H}, x=c_1(p_1, \ldots, p_k),\textbf{P}(p_{I_1}), \ldots, \textbf{P}(p_{I_l}) \;\;\vdash \;\; \textbf{P}(x) \qquad \ldots \qquad}{ \textbf{H} \;\;\vdash\;\; \textbf{P}(x) }</math>\|\| where <math>x</math> has inductive datatype <math>DT</math> as type and appears free in <math>\textbf{P}</math>; <math>\{p_{I_1}, \ldots, p_{I_l}\} \subseteq \{p_1, \ldots, p_k\}</math> are the inductive parameters (if any); an antecedent is created for every constructor <math>c_i</math> of <math>DT</math>; all parameters are introduced as fresh identifiers; examples [[Datatype Rules\|here]] \|\| M

	\|}		\|}

		+	See also [[Extension Proof Rules#Inference Rules]].

	[[Category:User documentation\|The Proving Perspective]]		[[Category:User documentation\|The Proving Perspective]]
	[[Category:Rodin Platform\|The Proving Perspective]]		[[Category:Rodin Platform\|The Proving Perspective]]
	[[Category:User manual\|The Proving Perspective]]		[[Category:User manual\|The Proving Perspective]]

←Older revision		Revision as of 07:29, 7 September 2010
(3 intermediate revisions not shown.)
Line 1:		Line 1:
-	{{Navigation\|Previous= [[~~Extending_the_Static_Checker~~(How_to_extend_Rodin_Tutorial)]] \| Up= [[Plug-in_Tutorial\|How to extend Rodin Tutorial (Index)]] \| Next= }}	+	{{Navigation\|Previous= [[Providing_help_for_your_plug-in_(How_to_extend_Rodin_Tutorial) \| Providing help]] \| Up= [[Plug-in_Tutorial\|How to extend Rodin Tutorial (Index)]] \| Next= [[Extending_the_Proof_Obligation_Generator(How_to_extend_Rodin_Tutorial) \| Generating the proof obligations]]}}

	=== In this part ===		=== In this part ===
Line 257:		Line 257:
	}		}

-		+	{{Navigation\|Previous= [[Providing_help_for_your_plug-in_(How_to_extend_Rodin_Tutorial) \| Providing help]] \| Up= [[Plug-in_Tutorial\|How to extend Rodin Tutorial (Index)]] \| Next= [[Extending_the_Proof_Obligation_Generator(How_to_extend_Rodin_Tutorial) \| Generating the proof obligations]]}}
-	{{Navigation\|Previous= [[~~Extending_the_Static_Checker~~(How_to_extend_Rodin_Tutorial)]] \| Up= [[Plug-in_Tutorial\|How to extend Rodin Tutorial (Index)]] \| Next= }}	+

	[[Category:Developer documentation\|*Index]]		[[Category:Developer documentation\|*Index]]
	[[Category:Rodin Platform\|*Index]]		[[Category:Rodin Platform\|*Index]]
	[[Category:Tutorial\|*Index]]		[[Category:Tutorial\|*Index]]

←Older revision		Revision as of 07:14, 7 September 2010
Line 120:		Line 120:
	As we had a detailed view (captures) of all the actions further needed, the next parts of this tutorial will focus only on the extensions.		As we had a detailed view (captures) of all the actions further needed, the next parts of this tutorial will focus only on the extensions.

-	{{Navigation\|Previous= [[Creating_a_new_plug-in_using_eclipse_(How_to_extend_Rodin_Tutorial)\|Creating our plug-in]]\|Next= [[Extend_Rodin_Structured_Editor_(How_to_extend_Rodin_Tutorial)\|~~Extend~~ the structured editor]] \| Up= [[Plug-in_Tutorial\|How to extend Rodin Tutorial (Index)]]}}	+	{{Navigation\|Previous= [[Creating_a_new_plug-in_using_eclipse_(How_to_extend_Rodin_Tutorial)\|Creating our plug-in]]\|Next= [[Extend_Rodin_Structured_Editor_(How_to_extend_Rodin_Tutorial)\|Extending the structured editor]] \| Up= [[Plug-in_Tutorial\|How to extend Rodin Tutorial (Index)]]}}

	[[Category:Developer documentation\|*Index]]		[[Category:Developer documentation\|*Index]]
	[[Category:Rodin Platform\|*Index]]		[[Category:Rodin Platform\|*Index]]
	[[Category:Tutorial\|*Index]]		[[Category:Tutorial\|*Index]]