Language of an Event-B Component - Revision history

imported>Tommy: /* Solution for Proofs */

2013-11-20T15:06:59Z

Solution for Proofs

← Older revision		Revision as of 15:06, 20 November 2013
Line 33:		Line 33:
	An [http://deploy-eprints.ecs.soton.ac.uk/464/ Event-B model] has been developed to prove that this factory sharing can be implemented soundly and serves as a specification of this optimization.		An [http://deploy-eprints.ecs.soton.ac.uk/464/ Event-B model] has been developed to prove that this factory sharing can be implemented soundly and serves as a specification of this optimization.

	The last degree of freedom is the choice of the formula factory stored at the root. In a stable model, all proof obligations and proofs are expressed in the same language. It is therefore the factory for this language that should be stored at the root of the proof file. The platform should always ensure that this factory is kept in ~~synch~~ with the corresponding proof obligation file.		The last degree of freedom is the choice of the formula factory stored at the root. In a stable model, all proof obligations and proofs are expressed in the same language. It is therefore the factory for this language that should be stored at the root of the proof file. The platform should always ensure that this factory is kept in sync with the corresponding proof obligation file.

	[[Category:Design]]		[[Category:Design]]
	[[Category:Rodin Platform]]		[[Category:Rodin Platform]]

imported>Tommy: /* General Solution */

2013-11-20T14:58:22Z

General Solution

← Older revision		Revision as of 14:58, 20 November 2013
Line 11:		Line 11:
	==General Solution==		==General Solution==

	The language information is implemented by an instance of {{class\|org.eventb.core.ast.FormulaFactory}}. Each instance contains a dedicated parser and type-checker which allows to transform a character string into a tree. Conversely, each formula tree has a formula factory attached to it which provides a way to transform it back into a string.		The language information is implemented by an instance of {{class\|org.eventb.core.ast.FormulaFactory}}. Each instance contains a dedicated parser and type-checker which allows to transform a character string into a tree (this operation is called de-serialization). Conversely, each formula tree has a formula factory attached to it which provides a way to transform it back into a string (this is operation is called serialization).

	All what is needed then is to know which formula factory to use for deserializing an Event-B component. For most files, this information is provided by the Theory plug-in, which contributes to the <tt>org.eventb.core.formulaExtensionProvider</tt> extension point. Given an Event-B root, the object contributed to this extension point returns the formula factory to use for parsing its contents.		All what is needed then is to know which formula factory to use for deserializing an Event-B component. For most files, this information is provided by the Theory plug-in, which contributes to the <tt>org.eventb.core.formulaExtensionProvider</tt> extension point. Given an Event-B root, the object contributed to this extension point returns the formula factory to use for parsing its contents.

imported>Tommy: /* General Solution */

2013-11-20T14:54:53Z

General Solution

← Older revision		Revision as of 14:54, 20 November 2013
Line 11:		Line 11:
	==General Solution==		==General Solution==

	The language information is implemented by an instance of {{class\|org.eventb.core.ast.FormulaFactory}}). Each instance contains a dedicated parser and type-checker which allows to transform a character string into a tree. Conversely, each formula tree has a formula factory attached to it which provides a way to transform it back into a string.		The language information is implemented by an instance of {{class\|org.eventb.core.ast.FormulaFactory}}. Each instance contains a dedicated parser and type-checker which allows to transform a character string into a tree. Conversely, each formula tree has a formula factory attached to it which provides a way to transform it back into a string.

	All what is needed then is to know which formula factory to use for deserializing an Event-B component. For most files, this information is provided by the Theory plug-in, which contributes to the <tt>org.eventb.core.formulaExtensionProvider</tt> extension point. Given an Event-B root, the object contributed to this extension point returns the formula factory to use for parsing its contents.		All what is needed then is to know which formula factory to use for deserializing an Event-B component. For most files, this information is provided by the Theory plug-in, which contributes to the <tt>org.eventb.core.formulaExtensionProvider</tt> extension point. Given an Event-B root, the object contributed to this extension point returns the formula factory to use for parsing its contents.

imported>Laurent: /* Solution for Proofs */ Fix link

2013-11-20T12:48:13Z

Solution for Proofs: Fix link

← Older revision		Revision as of 12:48, 20 November 2013
Line 31:		Line 31:
	However, this solution would waste a lot of space as most often all proofs would share the same formula factory. To mitigate this, we instead share a common formula factory at the root of the proof file, which is used by default by all proofs. For the proofs that are expressed in a different language, we store the formula factory in the proof node.		However, this solution would waste a lot of space as most often all proofs would share the same formula factory. To mitigate this, we instead share a common formula factory at the root of the proof file, which is used by default by all proofs. For the proofs that are expressed in a different language, we store the formula factory in the proof node.

	An [http://deploy-eprints.ecs.soton.ac.uk/464/~~1/ProofLanguage.zip~~ Event-B model] has been developed to prove that this factory sharing can be implemented soundly and serves as a specification of this optimization.		An [http://deploy-eprints.ecs.soton.ac.uk/464/ Event-B model] has been developed to prove that this factory sharing can be implemented soundly and serves as a specification of this optimization.

	The last degree of freedom is the choice of the formula factory stored at the root. In a stable model, all proof obligations and proofs are expressed in the same language. It is therefore the factory for this language that should be stored at the root of the proof file. The platform should always ensure that this factory is kept in synch with the corresponding proof obligation file.		The last degree of freedom is the choice of the formula factory stored at the root. In a stable model, all proof obligations and proofs are expressed in the same language. It is therefore the factory for this language that should be stored at the root of the proof file. The platform should always ensure that this factory is kept in synch with the corresponding proof obligation file.

imported>Laurent: /* Solution for Proofs */ add link to model

2013-11-20T12:46:47Z

Solution for Proofs: add link to model

← Older revision		Revision as of 12:46, 20 November 2013
Line 31:		Line 31:
	However, this solution would waste a lot of space as most often all proofs would share the same formula factory. To mitigate this, we instead share a common formula factory at the root of the proof file, which is used by default by all proofs. For the proofs that are expressed in a different language, we store the formula factory in the proof node.		However, this solution would waste a lot of space as most often all proofs would share the same formula factory. To mitigate this, we instead share a common formula factory at the root of the proof file, which is used by default by all proofs. For the proofs that are expressed in a different language, we store the formula factory in the proof node.

	An Event-B model has been developed to prove that this factory sharing can be implemented soundly and serves as a specification of this optimization.		An [http://deploy-eprints.ecs.soton.ac.uk/464/1/ProofLanguage.zip Event-B model] has been developed to prove that this factory sharing can be implemented soundly and serves as a specification of this optimization.

	The last degree of freedom is the choice of the formula factory stored at the root. In a stable model, all proof obligations and proofs are expressed in the same language. It is therefore the factory for this language that should be stored at the root of the proof file. The platform should always ensure that this factory is kept in synch with the corresponding proof obligation file.		The last degree of freedom is the choice of the formula factory stored at the root. In a stable model, all proof obligations and proofs are expressed in the same language. It is therefore the factory for this language that should be stored at the root of the proof file. The platform should always ensure that this factory is kept in synch with the corresponding proof obligation file.

imported>Laurent: First full version of design

2013-11-20T12:37:43Z

First full version of design

← Older revision		Revision as of 12:37, 20 November 2013
Line 1:		Line 1:
	{{TOCright}}		{{TOCright}}

	Since the introduction of mathematical extensions in Rodin 2.0, Event-B components can use extended version of the Event-B mathematical language. This ~~page described how this is organized~~ in ~~the core platform~~.		Since the introduction of mathematical extensions in Rodin 2.0, Event-B components can use extended version of the Event-B mathematical language. This change was implemented then, but there were some places where strange things could happen, weakening the confidence one can have in proofs.

	~~==Interface with~~ the ~~Theory Plug-in==~~		This design document describes how this has been implemented in a better way in the core platform for Rodin 3.0.

	For most files, the actual version of the Event-B language is provided by the Theory plug-in. This is done by contributing to the <tt>org.eventb.core.formulaExtensionProvider</tt> extension point. Given an Event-B root, the object contributed to this extension point provides the formula factory to use for parsing the contents of the file. In practice, all regular files share the same formula factory, thanks to the Theory Path. However, theory files can each have a separate formula factory.		==Requirement==

	~~==Language~~ of ~~Proofs==~~		All Event-B formulas are stored on disk as plain character strings in the Rodin database (i.e., in XML files). It is therefore necessary to know in which language they have been written to be able to parse them back to a tree in memory. Conversely, the serialization of Event-B formulas need to know how to transform the tree in memory into a character string.

	~~There is however a special case for proof files.~~		==General Solution==

			The language information is implemented by an instance of {{class\|org.eventb.core.ast.FormulaFactory}}). Each instance contains a dedicated parser and type-checker which allows to transform a character string into a tree. Conversely, each formula tree has a formula factory attached to it which provides a way to transform it back into a string.

			All what is needed then is to know which formula factory to use for deserializing an Event-B component. For most files, this information is provided by the Theory plug-in, which contributes to the <tt>org.eventb.core.formulaExtensionProvider</tt> extension point. Given an Event-B root, the object contributed to this extension point returns the formula factory to use for parsing its contents.

			Unchecked machine and context files are written directly by the end-user and are parsed using the formula factory of their project. If the language changes, it is up to the user to update this file to make it parseable again, if need be.

			As concerns generated files (e.g., statically checked files and proof obligation files), they contain formulas in the same language as the component from which they originate. Moreover, the Theory plug-in ensures that they are re-generated whenever the language of their respective component changes. This is implemented by adding a dependency in the Rodin builder to ensure that these files are considered obsolete when the language changes.

			Proof status files do not contain any formula and are therefore independent on the Event-B mathematical language.

			==Solution for Proofs==

			The last kind of files are proof files which are a bit more delicate. These files are also considered as written by the end-users (sometimes helped by the automated prover working on their behalf). However, their structure is quite intricate and it is not conceivable to have end-user editing them directly. Instead, users have the Proving UI for editing them in a friendly manner.

			As proofs are independent of the input component (machine or context), they need to have their own mechanism for retrieving their associated formula factory. This mechanism must be on a per proof basis, as proofs can be edited independently and therefore expressed in different languages across time.

			The simplest solution would therefore be to serialize in each proof the formula factory with which it was built so that it can be parsed back.

			However, this solution would waste a lot of space as most often all proofs would share the same formula factory. To mitigate this, we instead share a common formula factory at the root of the proof file, which is used by default by all proofs. For the proofs that are expressed in a different language, we store the formula factory in the proof node.

			An Event-B model has been developed to prove that this factory sharing can be implemented soundly and serves as a specification of this optimization.

			The last degree of freedom is the choice of the formula factory stored at the root. In a stable model, all proof obligations and proofs are expressed in the same language. It is therefore the factory for this language that should be stored at the root of the proof file. The platform should always ensure that this factory is kept in synch with the corresponding proof obligation file.

	[[Category:Design]]		[[Category:Design]]
	[[Category:Rodin Platform]]		[[Category:Rodin Platform]]

imported>Laurent at 11:14, 20 November 2013

2013-11-20T11:14:20Z

← Older revision		Revision as of 11:14, 20 November 2013
Line 7:		Line 7:
	For most files, the actual version of the Event-B language is provided by the Theory plug-in. This is done by contributing to the <tt>org.eventb.core.formulaExtensionProvider</tt> extension point. Given an Event-B root, the object contributed to this extension point provides the formula factory to use for parsing the contents of the file. In practice, all regular files share the same formula factory, thanks to the Theory Path. However, theory files can each have a separate formula factory.		For most files, the actual version of the Event-B language is provided by the Theory plug-in. This is done by contributing to the <tt>org.eventb.core.formulaExtensionProvider</tt> extension point. Given an Event-B root, the object contributed to this extension point provides the formula factory to use for parsing the contents of the file. In practice, all regular files share the same formula factory, thanks to the Theory Path. However, theory files can each have a separate formula factory.

	==Language of ~~Unchecked Components~~==		==Language of Proofs==

	~~==Language of Generated Files==~~		There is however a special case for proof files.

	~~==Language of Proofs==~~


	[[Category:Design]]		[[Category:Design]]
	[[Category:Rodin Platform]]		[[Category:Rodin Platform]]

imported>Laurent: /* Interface with the Theory Plug-in */

2013-11-20T11:13:05Z

Interface with the Theory Plug-in

← Older revision		Revision as of 11:13, 20 November 2013
Line 4:		Line 4:

	==Interface with the Theory Plug-in==		==Interface with the Theory Plug-in==

			For most files, the actual version of the Event-B language is provided by the Theory plug-in. This is done by contributing to the <tt>org.eventb.core.formulaExtensionProvider</tt> extension point. Given an Event-B root, the object contributed to this extension point provides the formula factory to use for parsing the contents of the file. In practice, all regular files share the same formula factory, thanks to the Theory Path. However, theory files can each have a separate formula factory.

	==Language of Unchecked Components==		==Language of Unchecked Components==

imported>Laurent: Layout

2013-11-20T11:10:01Z

Layout

New page

{{TOCright}}

Since the introduction of mathematical extensions in Rodin 2.0, Event-B components can use extended version of the Event-B mathematical language. This page described how this is organized in the core platform.

==Interface with the Theory Plug-in==

==Language of Unchecked Components==

==Language of Generated Files==

==Language of Proofs==

[[Category:Design]]
[[Category:Rodin Platform]]