ADVANCE D3.3 Language extension - Revision history

imported>Asiehsalehi: /* Planning */

2013-10-07T14:52:36Z

Planning

← Older revision		Revision as of 14:52, 7 October 2013
Line 41:		Line 41:
	The implementation of the Theory plug-in is now reaching a stable state. A lot of enhancement were introduced during June-August 2013, which makes the Theory plug-in ready to be integrated as a part of the core distribution of Rodin v2.8.		The implementation of the Theory plug-in is now reaching a stable state. A lot of enhancement were introduced during June-August 2013, which makes the Theory plug-in ready to be integrated as a part of the core distribution of Rodin v2.8.
	Also the following works are planned for the third period:		Also the following works are planned for the third period:
	* Enhancement of the deploy process: providing a read-only view of a deployed theory.		* Enhancement of the deploy process: providing a read-only view of a deployed theory
	* Improvements of the plugin structure in order to be supported by ProB		* Improvements of the plugin structure in order to be supported by ProB
	* Optimization of the HTML editor of a theory		* Optimization of the HTML editor of a theory

imported>Asiehsalehi: /* Planning */

2013-10-07T14:52:22Z

Planning

← Older revision		Revision as of 14:52, 7 October 2013
Line 40:		Line 40:

	The implementation of the Theory plug-in is now reaching a stable state. A lot of enhancement were introduced during June-August 2013, which makes the Theory plug-in ready to be integrated as a part of the core distribution of Rodin v2.8.		The implementation of the Theory plug-in is now reaching a stable state. A lot of enhancement were introduced during June-August 2013, which makes the Theory plug-in ready to be integrated as a part of the core distribution of Rodin v2.8.
			Also the following works are planned for the third period:
			* Enhancement of the deploy process: providing a read-only view of a deployed theory.
			* Improvements of the plugin structure in order to be supported by ProB
			* Optimization of the HTML editor of a theory
			** colour coding to be compatible with the Event-B editor
			** enhancing the view of the conditional rewrite rules
			* Providing a facility to automatic generation of rewrite/inference rules (from axiom/theorem)

	== References ==		== References ==

imported>Asiehsalehi: /* Motivations / Decisions */

2013-09-23T10:47:56Z

Motivations / Decisions

← Older revision		Revision as of 10:47, 23 September 2013
Line 9:		Line 9:
	Supporting mathematical and proof extensions has been a longing for the Event-B community for considerable time. Serious considerations have been made to ensure any support ensures: 1) ease of use, and 2) soundness preservation. The Theory plug-in became a natural candidate to provide support for mathematical and proof extensions. The use of proof obligations goes a long way in preserving the soundness of the underlying Event-B formalism.		Supporting mathematical and proof extensions has been a longing for the Event-B community for considerable time. Serious considerations have been made to ensure any support ensures: 1) ease of use, and 2) soundness preservation. The Theory plug-in became a natural candidate to provide support for mathematical and proof extensions. The use of proof obligations goes a long way in preserving the soundness of the underlying Event-B formalism.

	In the past 12 months, the capability of defining axiomatic definitions has been provided. Axiomatic definitions are defined by supplying the types, a set of operators, and a set of axioms. This feature has allowed us to create a few significant theories (language extensions), including the generalized sum/product and real numbers. Also it aids to model the hybrid systems.		In the past 12 months, the capability of defining axiomatic definitions has been provided. Axiomatic definitions are defined by supplying the types, a set of operators, and a set of axioms. This feature has allowed us to create a few significant theories (language extensions), including the generalized sum/product and real numbers. Also it aids to model the hybrid systems. These extensions are being evaluated in the WP1 and WP2 case studies.

	In the past 5 months, the procedure of accessibility scope definition is enhanced as below:		In the past 5 months, the procedure of accessibility scope definition is enhanced as below:

imported>Asiehsalehi: /* Motivations / Decisions */

2013-09-23T10:43:08Z

Motivations / Decisions

← Older revision		Revision as of 10:43, 23 September 2013
Line 8:		Line 8:

	Supporting mathematical and proof extensions has been a longing for the Event-B community for considerable time. Serious considerations have been made to ensure any support ensures: 1) ease of use, and 2) soundness preservation. The Theory plug-in became a natural candidate to provide support for mathematical and proof extensions. The use of proof obligations goes a long way in preserving the soundness of the underlying Event-B formalism.		Supporting mathematical and proof extensions has been a longing for the Event-B community for considerable time. Serious considerations have been made to ensure any support ensures: 1) ease of use, and 2) soundness preservation. The Theory plug-in became a natural candidate to provide support for mathematical and proof extensions. The use of proof obligations goes a long way in preserving the soundness of the underlying Event-B formalism.

			In the past 12 months, the capability of defining axiomatic definitions has been provided. Axiomatic definitions are defined by supplying the types, a set of operators, and a set of axioms. This feature has allowed us to create a few significant theories (language extensions), including the generalized sum/product and real numbers. Also it aids to model the hybrid systems.

	In the past 5 months, the procedure of accessibility scope definition is enhanced as below:		In the past 5 months, the procedure of accessibility scope definition is enhanced as below:
Line 17:		Line 19:

	* Conflict checking during process of importing a theory or introducing a theory.		* Conflict checking during process of importing a theory or introducing a theory.
	* Several bugs are fixed.		* Several bugs are fixed, including the colour coding.

	== Available Documentation ==		== Available Documentation ==

imported>Nicolas: Fix title levels

2013-08-27T12:36:41Z

Fix title levels

← Older revision		Revision as of 12:36, 27 August 2013
Line 1:		Line 1:
	= Overview =		== Overview ==

	Mathematical extensions have been co-developed by Systerel (for the Core Rodin Platform) and Southampton (for the Theory plug-in). The main purpose of this new feature was to provide the Rodin user with a way to extend the standard Event-B mathematical language by supporting user-defined operators, basic predicates and algebraic types. Along with these additional notations, the user can also define new proof rules (proof extensions).		Mathematical extensions have been co-developed by Systerel (for the Core Rodin Platform) and Southampton (for the Theory plug-in). The main purpose of this new feature was to provide the Rodin user with a way to extend the standard Event-B mathematical language by supporting user-defined operators, basic predicates and algebraic types. Along with these additional notations, the user can also define new proof rules (proof extensions).
Line 5:		Line 5:
	The Theory plug-in provides, among other things, a user-friendly mechanism to extend the Event-B mathematical language as well as the prover. A theory is the dedicated component used to hold mathematical extensions (datatypes, operators with direct definitions, operators with recursive definitions and operators with axiomatic definitions), and proof extensions (polymorphic theorems, rewrite and inference rules). Theories are developed in the workspace (akin to models), and are subject to static checking and proof obligation generation. Proof obligations generated from theories ensure any contributed extensions do not compromise the soundness of the existing infrastructure for modelling and proof. In essence, the Theory plug-in provides a systematic platform for defining, validating and using extensions while exploiting the benefits brought by proof obligations.		The Theory plug-in provides, among other things, a user-friendly mechanism to extend the Event-B mathematical language as well as the prover. A theory is the dedicated component used to hold mathematical extensions (datatypes, operators with direct definitions, operators with recursive definitions and operators with axiomatic definitions), and proof extensions (polymorphic theorems, rewrite and inference rules). Theories are developed in the workspace (akin to models), and are subject to static checking and proof obligation generation. Proof obligations generated from theories ensure any contributed extensions do not compromise the soundness of the existing infrastructure for modelling and proof. In essence, the Theory plug-in provides a systematic platform for defining, validating and using extensions while exploiting the benefits brought by proof obligations.

	= Motivations / Decisions =		== Motivations / Decisions ==

	Supporting mathematical and proof extensions has been a longing for the Event-B community for considerable time. Serious considerations have been made to ensure any support ensures: 1) ease of use, and 2) soundness preservation. The Theory plug-in became a natural candidate to provide support for mathematical and proof extensions. The use of proof obligations goes a long way in preserving the soundness of the underlying Event-B formalism.		Supporting mathematical and proof extensions has been a longing for the Event-B community for considerable time. Serious considerations have been made to ensure any support ensures: 1) ease of use, and 2) soundness preservation. The Theory plug-in became a natural candidate to provide support for mathematical and proof extensions. The use of proof obligations goes a long way in preserving the soundness of the underlying Event-B formalism.
Line 19:		Line 19:
	* Several bugs are fixed.		* Several bugs are fixed.

	= Available Documentation =		== Available Documentation ==

	Pre-studies (states of the art, proposals, discussions):		Pre-studies (states of the art, proposals, discussions):
Line 35:		Line 35:
	* Theory Plug-in User Manual.<ref>http://wiki.event-b.org/images/Theory_Plugin.pdf</ref>		* Theory Plug-in User Manual.<ref>http://wiki.event-b.org/images/Theory_Plugin.pdf</ref>

	= Planning =		== Planning ==

	The implementation of the Theory plug-in is now reaching a stable state. A lot of enhancement were introduced during June-August 2013, which makes the Theory plug-in ready to be integrated as a part of the core distribution of Rodin v2.8.		The implementation of the Theory plug-in is now reaching a stable state. A lot of enhancement were introduced during June-August 2013, which makes the Theory plug-in ready to be integrated as a part of the core distribution of Rodin v2.8.

	= References =		== References ==
	<references/>		<references/>

	[[Category:ADVANCE D3.3 Deliverable]]		[[Category:ADVANCE D3.3 Deliverable]]

imported>Asiehsalehi: /* Planning */

2013-08-22T15:32:47Z

Planning

← Older revision		Revision as of 15:32, 22 August 2013
Line 36:		Line 36:

	= Planning =		= Planning =
	~~{{TODO}}~~
			The implementation of the Theory plug-in is now reaching a stable state. A lot of enhancement were introduced during June-August 2013, which makes the Theory plug-in ready to be integrated as a part of the core distribution of Rodin v2.8.

	= References =		= References =

imported>Asiehsalehi: /* Motivations / Decisions */

2013-08-22T15:30:18Z

Motivations / Decisions

← Older revision		Revision as of 15:30, 22 August 2013
Line 9:		Line 9:
	Supporting mathematical and proof extensions has been a longing for the Event-B community for considerable time. Serious considerations have been made to ensure any support ensures: 1) ease of use, and 2) soundness preservation. The Theory plug-in became a natural candidate to provide support for mathematical and proof extensions. The use of proof obligations goes a long way in preserving the soundness of the underlying Event-B formalism.		Supporting mathematical and proof extensions has been a longing for the Event-B community for considerable time. Serious considerations have been made to ensure any support ensures: 1) ease of use, and 2) soundness preservation. The Theory plug-in became a natural candidate to provide support for mathematical and proof extensions. The use of proof obligations goes a long way in preserving the soundness of the underlying Event-B formalism.

	In the past 5 months, the ~~development~~ of ~~the Theory plug-in resulted in a new~~ scope definition ~~procedure~~ as ~~following~~:		In the past 5 months, the procedure of accessibility scope definition is enhanced as below:

	* A theory can access other global theories directly.		* A theory can access other global theories directly.

imported>Asiehsalehi: /* Motivations / Decisions */

2013-08-22T15:28:15Z

Motivations / Decisions

← Older revision		Revision as of 15:28, 22 August 2013
Line 12:		Line 12:

	* A theory can access other global theories directly.		* A theory can access other global theories directly.
	* A theory (wither local/global) will be introduced to a context/machine scope by means of "theorypath" file.		* A theory (wither local/global) will be introduced to a context/machine scope by means of a "theorypath" file.

	Also the below additions are added to the plug-in:		Also the below additions are added to the plug-in:

imported>Asiehsalehi: /* Motivations / Decisions */

2013-08-22T15:27:54Z

Motivations / Decisions

← Older revision		Revision as of 15:27, 22 August 2013
Line 6:		Line 6:

	= Motivations / Decisions =		= Motivations / Decisions =
	~~{{TODO}}~~
			Supporting mathematical and proof extensions has been a longing for the Event-B community for considerable time. Serious considerations have been made to ensure any support ensures: 1) ease of use, and 2) soundness preservation. The Theory plug-in became a natural candidate to provide support for mathematical and proof extensions. The use of proof obligations goes a long way in preserving the soundness of the underlying Event-B formalism.

			In the past 5 months, the development of the Theory plug-in resulted in a new scope definition procedure as following:

			* A theory can access other global theories directly.
			* A theory (wither local/global) will be introduced to a context/machine scope by means of "theorypath" file.

			Also the below additions are added to the plug-in:

			* Conflict checking during process of importing a theory or introducing a theory.
			* Several bugs are fixed.

	= Available Documentation =		= Available Documentation =

imported>Asiehsalehi: /* Available Documentation */

2013-08-22T14:01:58Z

Available Documentation

← Older revision		Revision as of 14:01, 22 August 2013
Line 22:		Line 22:

	User's guides:		User's guides:
	* Theory Plug-in User Manual.<ref>~~http://~~http://wiki.event-b.org/images/Theory_Plugin.pdf</ref>		* Theory Plug-in User Manual.<ref>http://wiki.event-b.org/images/Theory_Plugin.pdf</ref>

	= Planning =		= Planning =