Mathematical Language Evolution Design - Revision history

imported>Nicolas: /* Changes to client code */

2009-05-11T09:40:53Z

Changes to client code

← Older revision		Revision as of 09:40, 11 May 2009
Line 261:		Line 261:
	E = F		E = F

	In PP Translator rules that concern <math>\id, \prjone, \prjtwo</math> are changed so that they take generic operators as input (see ppTrans documentation, rules IR39, IR43, IR44).		In PP Translator, rules that concern <math>\id, \prjone, \prjtwo</math> are changed so that they take generic operators as input (see ppTrans documentation, rules IR39, IR43, IR44).

			=== Expanders ===

			The new Partition predicate needed to be processed by the translator and the sequent prover, performing essentially the same job: to rewrite a partition predicate into its definition.
			To that purpose, a common framework of Expanders was implemented. Expanders aim at rewriting ("expanding") the definitions of some mathematical operators. For the time being, only a partition expander exists, but others may follow.

			Thus, a new rule was implemented to translate partition into its definition (see ppTrans documentation, rule BR8).

			In the prover, a tactic "org.eventb.core.seqprover.partitionRewriteTac" is added as part of the default auto-tactics. It can also be applied manually in the prover ui by clicking a "partition" in a formula.

	~~{{TODO\|talk about partition}}~~


	[[Category:Event-B]]		[[Category:Event-B]]
	[[Category:Design]]		[[Category:Design]]

imported>Laurent: /* Changes to client code */

2009-04-23T15:40:04Z

Changes to client code

← Older revision		Revision as of 15:40, 23 April 2009
Line 252:		Line 252:
	== Changes to client code ==		== Changes to client code ==

	Client code based on the "Formula.tom" file ~~prodived~~ in the AST package can now use the "FormulaV2.tom" file instead to take the syntax modifications into account. However, the former file is left unchanged to allow clients to keep on using it and decide whether and when to upgrade their code to V2.		Client code based on the "Formula.tom" file provided in the AST package can now use the "FormulaV2.tom" file instead to take the syntax modifications into account. However, the former file is left unchanged to allow clients to keep on using it and decide whether and when to upgrade their code to V2.

	In the sequent prover, the tactic that used to rewrite		In the sequent prover, the tactic that used to rewrite

imported>Laurent: /* Upgrade */

2009-04-23T15:38:51Z

Upgrade

← Older revision		Revision as of 15:38, 23 April 2009
Line 93:		Line 93:
	* it contains an identifier named "partition" (that would conflict with the new predicate of the same name)		* it contains an identifier named "partition" (that would conflict with the new predicate of the same name)

	In these cases an upgrade procedure has to be applied to the formula, in order to make it parseable with V2 mathematical ~~manguage~~.		In these cases an upgrade procedure has to be applied to the formula, in order to make it parseable with V2 mathematical language.
	It consists in rewriting KPRJ1, KPRJ2, KID expressions into their generic equivalent (see [[Changes to the Mathematical Language of Event-B#Generic Identity and Projections]]).		It consists in rewriting KPRJ1, KPRJ2, KID expressions into their generic equivalent (see [[Changes to the Mathematical Language of Event-B#Generic Identity and Projections]]).
	For parentheses, the difference is only visible in a string representation, where the missing ones are added by the {{method\|toString()}} method.		For parentheses, the difference is only visible in a string representation, where the missing ones are added by the {{method\|toString()}} method.

imported>Laurent: /* Upgrade */

2009-04-23T15:35:34Z

Upgrade

← Older revision		Revision as of 15:35, 23 April 2009
Line 93:		Line 93:
	* it contains an identifier named "partition" (that would conflict with the new predicate of the same name)		* it contains an identifier named "partition" (that would conflict with the new predicate of the same name)

	In these cases an upgrade procedure has to be applied to the formula, in order to make it ~~parse~~ with V2 mathematical manguage.		In these cases an upgrade procedure has to be applied to the formula, in order to make it parseable with V2 mathematical manguage.
	It consists in rewriting KPRJ1, KPRJ2, KID expressions into their generic equivalent (see [[Changes to the Mathematical Language of Event-B#Generic Identity and Projections]]).		It consists in rewriting KPRJ1, KPRJ2, KID expressions into their generic equivalent (see [[Changes to the Mathematical Language of Event-B#Generic Identity and Projections]]).
	For parentheses, the difference is only visible in a string representation, where the missing ones are added by the {{method\|toString()}} method.		For parentheses, the difference is only visible in a string representation, where the missing ones are added by the {{method\|toString()}} method.

imported>Nicolas: /* Sequent Prover */

2009-04-20T13:01:09Z

Sequent Prover

← Older revision		Revision as of 13:01, 20 April 2009
Line 250:		Line 250:
	In the upgrade result, that will appear as a problem of kind {{class\|ProblemKind.notUpgradableError}}.		In the upgrade result, that will appear as a problem of kind {{class\|ProblemKind.notUpgradableError}}.

	== ~~Sequent Prover~~ ==		== Changes to client code ==
	{{TODO}}
			Client code based on the "Formula.tom" file prodived in the AST package can now use the "FormulaV2.tom" file instead to take the syntax modifications into account. However, the former file is left unchanged to allow clients to keep on using it and decide whether and when to upgrade their code to V2.

			In the sequent prover, the tactic that used to rewrite
			E ↦ F ∈ id(S) into
			E ∈ S ∧ F = E
			now rewrites
			E ↦ F ∈ id into
			E = F

			In PP Translator rules that concern <math>\id, \prjone, \prjtwo</math> are changed so that they take generic operators as input (see ppTrans documentation, rules IR39, IR43, IR44).


			{{TODO\|talk about partition}}


	[[Category:Event-B]]		[[Category:Event-B]]
	[[Category:Design]]		[[Category:Design]]

imported>Nicolas: /* Upgrade */

2009-04-20T12:40:24Z

Upgrade

← Older revision		Revision as of 12:40, 20 April 2009
Line 87:		Line 87:
	== Upgrade ==		== Upgrade ==

	Formulas written with version {{class\|V1}} will need upgrading to version {{class\|V2}}. However, ~~most of the~~ V1 formulas will be exactly the same ~~with~~ V2.		Formulas written with version {{class\|V1}} will need upgrading to version {{class\|V2}}. However, many V1 formulas will be exactly the same in V2.
	A formula needs ugrading if:		A formula needs ugrading if:
	* it contains one of {KPRJ1, KPRJ2, KID}		* it contains one of {KPRJ1, KPRJ2, KID}
	* it contains a non parenthesised sequence of relational set operators		* it contains a non parenthesised sequence of relational set operators
			* it contains an identifier named "partition" (that would conflict with the new predicate of the same name)

	In these cases an upgrade procedure ~~will~~ be applied to the formula ~~using a {{class\|IFormulaRewriter}}~~, to ~~rewrite~~ KPRJ1, KPRJ2, KID expressions into their generic equivalent (see [[Changes to the Mathematical Language of Event-B#Generic Identity and Projections]]).		In these cases an upgrade procedure has to be applied to the formula, in order to make it parse with V2 mathematical manguage.
			It consists in rewriting KPRJ1, KPRJ2, KID expressions into their generic equivalent (see [[Changes to the Mathematical Language of Event-B#Generic Identity and Projections]]).
			For parentheses, the difference is only visible in a string representation, where the missing ones are added by the {{method\|toString()}} method.
			Bound identifiers named "partition" are renamed "partition1".

	Upgraded formulas can be obtained from a formula string by calling one of the new {{class\|FormulaFactory}}{{method\|.upgrade()}} methods. This will return a {{class\|IUpgradeResult}} as described below.
			Upgraded formulas can be obtained from a formula string by calling one of the new {{class\|FormulaFactory}}{{method\|.upgrade()}} methods. This will return a {{class\|IUpgradeResult}} as described [[#Upgrade result\|below]].


			Please notice that the version of a formula is not known by the {{class\|Formula}} object itself. Instead, one has to know, before parsing or upgrading a formula string, which version of the mathematical language is has been written with. If the string is extracted from a {{class\|RodinFile}}, it may be guessed from the file version (see [[#File upgrade]]).

	=== Upgrade result ===		=== Upgrade result ===

	{{~~TODO~~}}		{{class\|FormulaFactory}}{{method\|.upgrade()}} methods return a {{class\|IUpgradeResult}} that can be queried for:
			* whether or not the upgrade is a success
			* problems that occurred while attempting the upgrade
			* the upgraded formula, if upgrade succeeded

	=== File upgrade ===		=== File upgrade ===
Line 223:		Line 234:
	==== Identifiers named "partition" ====		==== Identifiers named "partition" ====

	{{~~TODO~~}}		Identifiers named "partition" will conflict with the new "partition" predicate if the formula does not rename them.
			But we cannot always rename an identifier in a formula without breaking things outside.

			Thus, free identifiers will not be renamed. This is a [[#Not upgradable cases\|not upgradable case]].

			Concerning bound identifiers, we simply have to rename them as "partition1". The {{method\|toString()}} method deals with alpha conversion if a bound identifier "partition1" already exists.

	==== Not upgradable cases ====		==== Not upgradable cases ====
Line 232:		Line 248:
	* the formula contains a "partition" free identifier		* the formula contains a "partition" free identifier

			In the upgrade result, that will appear as a problem of kind {{class\|ProblemKind.notUpgradableError}}.
	{{~~TODO~~}}

	== Sequent Prover ==		== Sequent Prover ==

imported>Nicolas: /* Upgrade */

2009-04-20T10:37:28Z

Upgrade

← Older revision		Revision as of 10:37, 20 April 2009
Line 94:		Line 94:
	In these cases an upgrade procedure will be applied to the formula using a {{class\|IFormulaRewriter}}, to rewrite KPRJ1, KPRJ2, KID expressions into their generic equivalent (see [[Changes to the Mathematical Language of Event-B#Generic Identity and Projections]]).		In these cases an upgrade procedure will be applied to the formula using a {{class\|IFormulaRewriter}}, to rewrite KPRJ1, KPRJ2, KID expressions into their generic equivalent (see [[Changes to the Mathematical Language of Event-B#Generic Identity and Projections]]).

	Upgraded formulas can be obtained from a formula string by calling one of the new {{class\|FormulaFactory}}{{method\|.upgrade()}} methods.		Upgraded formulas can be obtained from a formula string by calling one of the new {{class\|FormulaFactory}}{{method\|.upgrade()}} methods. This will return a {{class\|IUpgradeResult}} as described below.

			=== Upgrade result ===

			{{TODO}}

	=== File upgrade ===		=== File upgrade ===

imported>Nicolas: /* Not upgradable cases */

2009-04-20T10:35:06Z

Not upgradable cases

← Older revision		Revision as of 10:35, 20 April 2009
Line 216:		Line 216:
	\|<math>x \domres \id</math>		\|<math>x \domres \id</math>
	\|}		\|}

			==== Identifiers named "partition" ====

			{{TODO}}

	==== Not upgradable cases ====		==== Not upgradable cases ====

			In some situations, an upgrade would be needed (the formula contains <math>\id</math>, <math>\prjone,</math> <math>\prjtwo</math>, a "partition" bound identifier or lacks parentheses) but it is simply not possible to achieve it.
			Those cases are:
			* the formula string does not parse
			* the formula contains a "partition" free identifier


	{{TODO}}		{{TODO}}

imported>Nicolas: /* Upgrade */

2009-04-20T10:10:01Z

Upgrade

← Older revision		Revision as of 10:10, 20 April 2009
Line 94:		Line 94:
	In these cases an upgrade procedure will be applied to the formula using a {{class\|IFormulaRewriter}}, to rewrite KPRJ1, KPRJ2, KID expressions into their generic equivalent (see [[Changes to the Mathematical Language of Event-B#Generic Identity and Projections]]).		In these cases an upgrade procedure will be applied to the formula using a {{class\|IFormulaRewriter}}, to rewrite KPRJ1, KPRJ2, KID expressions into their generic equivalent (see [[Changes to the Mathematical Language of Event-B#Generic Identity and Projections]]).

	Upgraded formulas can be obtained from a formula string by calling one of the new {{class\|FormulaFactory}} {{method\|upgrade}} methods.		Upgraded formulas can be obtained from a formula string by calling one of the new {{class\|FormulaFactory}}{{method\|.upgrade()}} methods.

	=== File upgrade ===		=== File upgrade ===
Line 182:		Line 182:
	==== Typing generic operators ====		==== Typing generic operators ====

	{{~~TODO~~}}		The problem of typing generic operators arises when upgrading a fomula like <math>\operatorname{id(x)}</math>.
			We know that, in the general case, the upgraded version is <math>x \domres \id</math>.
			But which type should the generic <math>\id</math> bear ?

			An answer is:
			If the V1 operator is typed, then the V2 generic one should bear the same type.

			Given the convention that <math>\operatorname{o}_T</math> means that <math>\operatorname{o}</math> has type <math>T</math>, this entails rewriting <math>\id_{T}(x)</math> into <math>x \domres \id_{T}</math>.

			But then, what happens if <math>x</math> is a type expression,like <math>\mathbb{Z}</math> ?

			We would come to rewriting <math>\id_{\mathbb{P}(\mathbb{Z}\times\mathbb{Z})}(\mathbb{Z})</math> into <math>\mathbb{Z} \domres \id_{\mathbb{P}(\mathbb{Z}\times\mathbb{Z})}</math>.

			In this case, the domain restriction is clearly superfluous. This brings in a new rule:
			If the V1 unary operator has a type expression for argument, then the V2 generic atomic one needs no domain restriction

	{\| ~~border~~="4"		Putting things together, the following table summarizes the upgrade of generic operators, based on the <math>\id</math> operator example. Similar rules apply to <math>\prjone</math> and <math>\prjtwo</math>.
	~~\|+ Generic operator rewriting example~~		{\| cellspacing="10" cellpadding="10" style="text-align:center;"
	! scope=col \|		! scope=col \|
	! scope=col \|Math V1		! scope=col \|Math V1
Line 191:		Line 205:
	\|-		\|-
	! scope=row \|Type expression		! scope=row \|Type expression
	\|<math>\~~operatorname~~{~~id_~~{\mathbb{Z}}}(\mathbb{Z})</math>		\|<math>\id_{\mathbb{P}(\mathbb{Z}\times\mathbb{Z})}(\mathbb{Z})</math>
	\|<math>\~~operatorname~~{~~id_~~{\mathbb{Z}}}</math>		\|<math>\id_{\mathbb{P}(\mathbb{Z}\times\mathbb{Z})}</math>
	\|-		\|-
	! scope=row \|Typed		! scope=row \|Typed
	\|<math>\~~operatorname{~~id_{~~\mathbb{Z}}~~}(x)</math>		\|<math>\id_{T}(x)</math>
	\|<math>x \~~domres_{~~\~~mathbb{Z}} \operatorname{~~id_{~~\mathbb{Z}}~~}</math>		\|<math>x \domres \id_{T}</math>
	\|-		\|-
	! scope=row \|Not typed		! scope=row \|Not typed
	\|<math>\~~operatorname{~~id(x)}</math>		\|<math>\id(x)</math>
	\|<math>x \domres \~~operatorname{~~id}</math>		\|<math>x \domres \id</math>
	\|}		\|}

Line 206:		Line 220:

	{{TODO}}		{{TODO}}


	== Sequent Prover ==		== Sequent Prover ==

imported>Nicolas: /* Typing generic operators */

2009-04-17T17:01:52Z

Typing generic operators

← Older revision		Revision as of 17:01, 17 April 2009
Line 183:		Line 183:

	{{TODO}}		{{TODO}}

			{\| border="4"
			\|+ Generic operator rewriting example
			! scope=col \|
			! scope=col \|Math V1
			! scope=col \|Math V2
			\|-
			! scope=row \|Type expression
			\|<math>\operatorname{id_{\mathbb{Z}}}(\mathbb{Z})</math>
			\|<math>\operatorname{id_{\mathbb{Z}}}</math>
			\|-
			! scope=row \|Typed
			\|<math>\operatorname{id_{\mathbb{Z}}}(x)</math>
			\|<math>x \domres_{\mathbb{Z}} \operatorname{id_{\mathbb{Z}}}</math>
			\|-
			! scope=row \|Not typed
			\|<math>\operatorname{id(x)}</math>
			\|<math>x \domres \operatorname{id}</math>
			\|}

	==== Not upgradable cases ====		==== Not upgradable cases ====