ADVANCE D3.2 Language extension - Revision history

imported>Tommy: /* Planning */

2012-06-29T08:33:46Z

Planning

← Older revision		Revision as of 08:33, 29 June 2012
Line 30:		Line 30:

	= Planning =		= Planning =
	The implementation of the Theory plug-in is now reaching a stable state. A lot of enhancement were introduced in June and July 2012 so that an integration in Rodin 2.6 was considered hasty and inappropriate. Thus, the Theory plug-in will become part of the core distribution of Rodin from version 2.7 which is planned for the end of October 2012.		The implementation of the Theory plug-in is now reaching a stable state. A lot of enhancement were introduced in June and July 2012 so that an integration in Rodin 2.6 (which code freeze was set by mid July) was considered hasty and inappropriate. Thus, the Theory plug-in will become part of the core distribution of Rodin from version 2.7 which is planned for the end of October 2012.

	= References =		= References =

imported>Tommy: /* Planning */

2012-06-29T08:32:28Z

Planning

← Older revision		Revision as of 08:32, 29 June 2012
Line 30:		Line 30:

	= Planning =		= Planning =
	The Theory plug-in ~~became~~ part of the core distribution of Rodin ~~since~~ version 2.6.		The implementation of the Theory plug-in is now reaching a stable state. A lot of enhancement were introduced in June and July 2012 so that an integration in Rodin 2.6 was considered hasty and inappropriate. Thus, the Theory plug-in will become part of the core distribution of Rodin from version 2.7 which is planned for the end of October 2012.

	= References =		= References =

imported>Tommy: /* Motivations / Decisions */

2012-06-29T08:27:26Z

Motivations / Decisions

← Older revision		Revision as of 08:27, 29 June 2012
Line 11:		Line 11:
	* Support for polymorphic theorems in proofs: theorems can be used to ensure the operator and datatype definitions capture the intended understanding by the theory developer. However, requests have been made to ensure that theorems are accessible for proofs. It was decided to provide a user interface-based wizard for instantiating the type parameters in order to 'localise' the theorem based on the current sequent.		* Support for polymorphic theorems in proofs: theorems can be used to ensure the operator and datatype definitions capture the intended understanding by the theory developer. However, requests have been made to ensure that theorems are accessible for proofs. It was decided to provide a user interface-based wizard for instantiating the type parameters in order to 'localise' the theorem based on the current sequent.
	* Added support of axiomatic definitions: as of version 1.3.2 of the Theory plug-in, only direct and recursive definitions for operators are possible. Requests have been made to add support for axiomatic operator definitions, which can open the door for sophisticated type definitions, e.g., the definition of REALS as an ordered ring with addition and multiplication.		* Added support of axiomatic definitions: as of version 1.3.2 of the Theory plug-in, only direct and recursive definitions for operators are possible. Requests have been made to add support for axiomatic operator definitions, which can open the door for sophisticated type definitions, e.g., the definition of REALS as an ordered ring with addition and multiplication.
	* From version 2.6 of Rodin, the Theory plug-in will ship as part of the core distribution. This particular decision was made given the maturity of the plug-in and its potential usefulness.		* From version 2.7 of Rodin, the Theory plug-in will ship as part of the core distribution. This particular decision was made given the maturity of the plug-in and its potential usefulness.

	= Available Documentation =		= Available Documentation =

imported>Tommy at 17:01, 25 June 2012

2012-06-25T17:01:03Z

← Older revision		Revision as of 17:01, 25 June 2012
Line 2:		Line 2:
	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).

	The Theory ~~plugin~~ 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 ~~plugin~~ 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. Earlier versions of the Theory ~~plugin~~ provided support for rewrite rules where soundness is preserved by means of proof obligations. The Theory ~~plugin~~ 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. Earlier versions of the Theory plug-in provided support for rewrite rules where soundness is preserved by means of proof obligations. 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 9 months, the development of the Theory ~~plugin~~ resulted in the following additions:		In the past 9 months, the development of the Theory plug-in resulted in the following additions:

	* Support for polymorphic theorems in proofs: theorems can be used to ensure the operator and datatype definitions capture the intended understanding by the theory developer. However, requests have been made to ensure that theorems are accessible for proofs. It was decided to provide a user interface-based wizard for instantiating the type parameters in order to 'localise' the theorem based on the current sequent.		* Support for polymorphic theorems in proofs: theorems can be used to ensure the operator and datatype definitions capture the intended understanding by the theory developer. However, requests have been made to ensure that theorems are accessible for proofs. It was decided to provide a user interface-based wizard for instantiating the type parameters in order to 'localise' the theorem based on the current sequent.
	* Added support of axiomatic definitions: as of version 1.3.2 of the Theory ~~plugin~~, only direct and recursive definitions for operators are possible. Requests have been made to add support for axiomatic operator definitions, which can open the door for sophisticated type definitions, e.g., the definition of REALS as an ordered ring with addition and multiplication.		* Added support of axiomatic definitions: as of version 1.3.2 of the Theory plug-in, only direct and recursive definitions for operators are possible. Requests have been made to add support for axiomatic operator definitions, which can open the door for sophisticated type definitions, e.g., the definition of REALS as an ordered ring with addition and multiplication.
	* From version 2.6 of Rodin, the Theory ~~plugin~~ will ship as part of the core distribution. This particular decision was made given the maturity of the ~~plugin~~ and its potential usefulness.		* From version 2.6 of Rodin, the Theory plug-in will ship as part of the core distribution. This particular decision was made given the maturity of the plug-in and its potential usefulness.

	= Available Documentation =		= Available Documentation =
Line 30:		Line 30:

	= Planning =		= Planning =
	The Theory ~~plugin~~ became part of the core distribution of Rodin since version 2.6.		The Theory plug-in became part of the core distribution of Rodin since version 2.6.

	= References =		= References =

imported>Tommy: /* Available Documentation */

2012-06-25T16:59:09Z

Available Documentation

← Older revision		Revision as of 16:59, 25 June 2012
Line 14:		Line 14:

	= Available Documentation =		= Available Documentation =
	~~Pre-studies (states of the art, proposals, discussions).~~

	* Proposals for Mathematical Extensions for Event-B<ref>http://deploy-eprints.ecs.soton.ac.uk/216/</ref>		Pre-studies (states of the art, proposals, discussions):
			* Proposals for Mathematical Extensions for Event-B.<ref>http://deploy-eprints.ecs.soton.ac.uk/216/</ref>
			* Mathematical Extension in Event-B through the Rodin Theory Component.<ref>http://deploy-eprints.ecs.soton.ac.uk/251/</ref>
			* Generic Parser's Design Alternatives.<ref>http://wiki.event-b.org/index.php/Constrained_Dynamic_Parser#Design_Alternatives</ref>

	* ~~Mathematical Extension in Event~~-~~B through the Rodin Theory Component~~<ref>http://~~deploy~~-~~eprints~~.~~ecs~~.~~soton~~.ac.uk/~~251~~/</ref>		Technical details (specifications):
			* Mathematical_Extensions wiki page.<ref>http://wiki.event-b.org/index.php/Mathematical_Extensions</ref>
			* Constrained Dynamic Lexer wiki page.<ref>http://wiki.event-b.org/index.php/Constrained_Dynamic_Lexer</ref>
			* Constrained Dynamic Parser wiki page.<ref>http://wiki.event-b.org/index.php/Constrained_Dynamic_Parser </ref>
			* Theory plug-in wiki page.<ref>http://wiki.event-b.org/index.php/Theory_Plug-in</ref>

	* Generic Parser's Design Alternatives<ref>http://wiki.event-b.org/index.php/Constrained_Dynamic_Parser#Design_Alternatives</ref>		User's guides:
			* Theory Plug-in User Manual.<ref>http://wiki.event-b.org/images/Theory_UM.pdf</ref>
	~~Technical details (specifications).~~

	* Mathematical_Extensions wiki page<ref>http://wiki.event-b.org/index.php/Mathematical_Extensions</ref>

	* Constrained Dynamic Lexer wiki page<ref>http://wiki.event-b.org/index.php/Constrained_Dynamic_Lexer</ref>

	* Constrained Dynamic Parser wiki page<ref>http://wiki.event-b.org/index.php/Constrained_Dynamic_Parser </ref>

	* Theory plug-in wiki page<ref>http://wiki.event-b.org/index.php/Theory_Plug-in</ref>

	User's guides.

	* Theory Plug-in User Manual<ref>http://wiki.event-b.org/images/Theory_UM.pdf</ref>

	= Planning =		= Planning =

imported>Tommy: /* Overview */

2012-06-25T16:05:46Z

Overview

← Older revision		Revision as of 16:05, 25 June 2012
Line 2:		Line 2:
	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).

	The Theory plugin provides, among other things, a user-friendly mechanism to extend the Event-B mathematical language as well as the prover. ~~The~~ theory component is 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 plugin provides a systematic platform for defining, validating and using extensions while exploiting the benefits brought by proof obligations.		The Theory plugin 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 plugin provides a systematic platform for defining, validating and using extensions while exploiting the benefits brought by proof obligations.

	= Motivations / Decisions =		= Motivations / Decisions =

imported>Tommy at 15:38, 25 June 2012

2012-06-25T15:38:00Z

← Older revision		Revision as of 15:38, 25 June 2012
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).

	The Theory plugin provides, among other things, a user-friendly mechanism to extend the Event-B mathematical language as well as the prover. The theory component is 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 plugin provides a systematic platform for defining, validating and using extensions while exploiting the benefits brought by proof obligations.		The Theory plugin provides, among other things, a user-friendly mechanism to extend the Event-B mathematical language as well as the prover. The theory component is 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 plugin 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. Earlier versions of the Theory plugin provided support for rewrite rules where soundness is preserved by means of proof obligations. The Theory plugin 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. Earlier versions of the Theory plugin provided support for rewrite rules where soundness is preserved by means of proof obligations. The Theory plugin 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 13:		Line 13:
	* From version 2.6 of Rodin, the Theory plugin will ship as part of the core distribution. This particular decision was made given the maturity of the plugin and its potential usefulness.		* From version 2.6 of Rodin, the Theory plugin will ship as part of the core distribution. This particular decision was made given the maturity of the plugin and its potential usefulness.

	== Available Documentation ==		= Available Documentation =
	Pre-studies (states of the art, proposals, discussions).		Pre-studies (states of the art, proposals, discussions).

Line 36:		Line 36:
	* Theory Plug-in User Manual<ref>http://wiki.event-b.org/images/Theory_UM.pdf</ref>		* Theory Plug-in User Manual<ref>http://wiki.event-b.org/images/Theory_UM.pdf</ref>

	== Planning ==		= Planning =
	The Theory plugin became part of the core distribution of Rodin since version 2.6.		The Theory plugin became part of the core distribution of Rodin since version 2.6.

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

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

imported>Tommy: /* Available Documentation */

2012-06-25T15:37:38Z

Available Documentation

← Older revision		Revision as of 15:37, 25 June 2012
Line 16:		Line 16:
	Pre-studies (states of the art, proposals, discussions).		Pre-studies (states of the art, proposals, discussions).

	* Proposals for Mathematical Extensions for Event-B <ref>http://deploy-eprints.ecs.soton.ac.uk/216/</ref>		* Proposals for Mathematical Extensions for Event-B<ref>http://deploy-eprints.ecs.soton.ac.uk/216/</ref>

	* Mathematical Extension in Event-B through the Rodin Theory Component<ref>http://deploy-eprints.ecs.soton.ac.uk/251/</ref>		* Mathematical Extension in Event-B through the Rodin Theory Component<ref>http://deploy-eprints.ecs.soton.ac.uk/251/</ref>

imported>Im06r: /* Motivations / Decisions */

2012-06-23T16:13:22Z

Motivations / Decisions

← Older revision		Revision as of 16:13, 23 June 2012
Line 5:		Line 5:

	== Motivations / Decisions ==		== Motivations / Decisions ==
	Supporting mathematical and proof extensions has been a longing for the Event-B community for considerable time ~~<ref>http://deploy-eprints.ecs.soton.ac.uk/216/</ref>~~. Serious considerations have been made to ensure any support ensures: 1) ease of use, and 2) soundness preservation. Earlier versions of the Theory plugin provided support for rewrite rules where soundness is preserved by means of proof obligations. The Theory plugin became a natural candidate to provide support for mathematical and proof extensions ~~<ref>http://deploy-eprints.ecs.soton.ac.uk/251/</ref>~~. 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. Earlier versions of the Theory plugin provided support for rewrite rules where soundness is preserved by means of proof obligations. The Theory plugin 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 9 months, the development of the Theory plugin resulted in the following additions:		In the past 9 months, the development of the Theory plugin resulted in the following additions:

imported>Im06r: /* Available Documentation */

2012-06-23T16:10:43Z

Available Documentation

← Older revision		Revision as of 16:10, 23 June 2012
Line 31:		Line 31:

	* Theory plug-in wiki page<ref>http://wiki.event-b.org/index.php/Theory_Plug-in</ref>		* Theory plug-in wiki page<ref>http://wiki.event-b.org/index.php/Theory_Plug-in</ref>

	* Records Extension Documentation on wiki<ref>http://wiki.event-b.org/index.php/Records_Extension</ref>

	User's guides.		User's guides.