D32 Mathematical Extensions - Revision history

imported>Tommy: /* Motivations */

2010-12-21T14:40:31Z

Motivations

← Older revision		Revision as of 14:40, 21 December 2010
Line 10:		Line 10:

	Main reasons for implementing mathematical extensions are:		Main reasons for implementing mathematical extensions are:
	* increased readability (<math>\;a\;\operatorname{OR}\;b\;</math> rather than <math>\;\operatorname{bool}(\;a=TRUE\;\or\;b=TRUE\;)</math>)		* increased readability ( <math>\;a\;\operatorname{OR}\;b\;</math> rather than <math>\;\operatorname{bool}(a=TRUE\;\or\;b=TRUE)</math>)
	* polymorphism (<math>l \in List(S \cprod T)</math>)		* polymorphism (<math>l \in List(S \cprod T)</math>)
	* decreased proving effort, thanks to extension specific proof rules instead of general purpose ones		* decreased proving effort, thanks to extension specific proof rules instead of general purpose ones

imported>Tommy: /* Motivations */

2010-12-21T14:39:56Z

Motivations

← Older revision		Revision as of 14:39, 21 December 2010
Line 10:		Line 10:

	Main reasons for implementing mathematical extensions are:		Main reasons for implementing mathematical extensions are:
	* increased readability (<math>a \; \operatorname{OR} \; b</math> rather than <math>\operatorname{bool}(a=TRUE \or b=TRUE)</math>)		* increased readability (<math>\;a\;\operatorname{OR}\;b\;</math> rather than <math>\;\operatorname{bool}(\;a=TRUE\;\or\;b=TRUE\;)</math>)
	* polymorphism (<math>l \in List(S \cprod T)</math>)		* polymorphism (<math>l \in List(S \cprod T)</math>)
	* decreased proving effort, thanks to extension specific proof rules instead of general purpose ones		* decreased proving effort, thanks to extension specific proof rules instead of general purpose ones

imported>Tommy at 13:04, 20 December 2010

2010-12-20T13:04:19Z

imported>Tommy at 10:15, 20 December 2010

2010-12-20T10:15:03Z

← Older revision		Revision as of 10:15, 20 December 2010
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 (prover 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 (prover extensions).
Line 7:		Line 7:
	Records Plug-in has been developed by University of Southampton before the mathematical extensions as a new feature to provide structured types in Event-B. The plug-in extends Rodin standard context editor with a new modelling construct to provide support for structured types, which can be defined in terms of two new clauses: record declarations and record extensions. Both enable users to define their custom reusable types, that are treated underline by Rodin as Event-B constant sets and relations, supported by additional axioms, which the plug-in generates to simplify the proofs.		Records Plug-in has been developed by University of Southampton before the mathematical extensions as a new feature to provide structured types in Event-B. The plug-in extends Rodin standard context editor with a new modelling construct to provide support for structured types, which can be defined in terms of two new clauses: record declarations and record extensions. Both enable users to define their custom reusable types, that are treated underline by Rodin as Event-B constant sets and relations, supported by additional axioms, which the plug-in generates to simplify the proofs.

	== Motivations ==		= Motivations =

	Main reasons for implementing mathematical extensions are:		Main reasons for implementing mathematical extensions are:
Line 18:		Line 18:
	The motivation for development of Records plug-in was to fill the gap in Event-B language - a missing support of a syntax for the direct definition of structured types. Some of the industrial partners expressed a desire to have this missing feature in Event-B, that would allow them to define their own structured types such as records or classes. Theoretically these structures could be modelled with existing Event-B capabilities via projection functions. Backed up by a refined theoretical proposal Records plug-in was developed to extend the standard Event-B notation with requested capability.		The motivation for development of Records plug-in was to fill the gap in Event-B language - a missing support of a syntax for the direct definition of structured types. Some of the industrial partners expressed a desire to have this missing feature in Event-B, that would allow them to define their own structured types such as records or classes. Theoretically these structures could be modelled with existing Event-B capabilities via projection functions. Backed up by a refined theoretical proposal Records plug-in was developed to extend the standard Event-B notation with requested capability.

	== Choices / Decisions ==		= Choices / Decisions =

	On the Core Rodin Platform side, implementing mathematical extensions required to make some parts of the code extensible, that were not designed to be so, namely the lexer and the parser. We were using tools that automatically generated them from a fixed grammar description, so we had to change to other technologies. A [http://wiki.event-b.org/index.php/Constrained_Dynamic_Parser study] has been made on available technologies. The Pratt algorithm was selected for its adequation with the purpose and it did not have the drawbacks of other technologies:		On the Core Rodin Platform side, implementing mathematical extensions required to make some parts of the code extensible, that were not designed to be so, namely the lexer and the parser. We were using tools that automatically generated them from a fixed grammar description, so we had to change to other technologies. A [http://wiki.event-b.org/index.php/Constrained_Dynamic_Parser study] has been made on available technologies. The Pratt algorithm was selected for its adequation with the purpose and it did not have the drawbacks of other technologies:
Line 32:		Line 32:
	Records plug-in required the extension of the Rodin database with the new constructs to support structured types. On the other hand the Event-B language itself did not support extension at that time. For that reason the decision was made to address extensibility problem at the lowest level possible, which was Rodin database, but to model structured types using standard Event-B notation at the level below. The translation from extended to standard syntax has been entrusted to the static checker, that was also extended for this purpose. Thus the plug-in provides the users with notation for record declarations and extensions in unchecked models, but the checked versions operate with standard Event-B constructs.		Records plug-in required the extension of the Rodin database with the new constructs to support structured types. On the other hand the Event-B language itself did not support extension at that time. For that reason the decision was made to address extensibility problem at the lowest level possible, which was Rodin database, but to model structured types using standard Event-B notation at the level below. The translation from extended to standard syntax has been entrusted to the static checker, that was also extended for this purpose. Thus the plug-in provides the users with notation for record declarations and extensions in unchecked models, but the checked versions operate with standard Event-B constructs.

	== Available Documentation ==		= Available Documentation =

	* Pre-studies (states of the art, proposals, discussions).		* Pre-studies (states of the art, proposals, discussions).
Line 49:		Line 49:
	** [http://wiki.event-b.org/images/Theory_UM.pdf]		** [http://wiki.event-b.org/images/Theory_UM.pdf]

	== Planning ==		= Planning =
	The Theory plug-in v2.1 is released. Work will continue on general maintenance, bug fixes as well adding new features as requested by the users of the plug-in.		The Theory plug-in v2.1 is released. Work will continue on general maintenance, bug fixes as well adding new features as requested by the users of the plug-in.


	[[Category:D32 Deliverable]]		[[Category:D32 Deliverable]]

imported>Tommy at 10:14, 20 December 2010

2010-12-20T10:14:23Z

← Older revision		Revision as of 10:14, 20 December 2010
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 (prover 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 (prover extensions).
Line 7:		Line 7:
	Records Plug-in has been developed by University of Southampton before the mathematical extensions as a new feature to provide structured types in Event-B. The plug-in extends Rodin standard context editor with a new modelling construct to provide support for structured types, which can be defined in terms of two new clauses: record declarations and record extensions. Both enable users to define their custom reusable types, that are treated underline by Rodin as Event-B constant sets and relations, supported by additional axioms, which the plug-in generates to simplify the proofs.		Records Plug-in has been developed by University of Southampton before the mathematical extensions as a new feature to provide structured types in Event-B. The plug-in extends Rodin standard context editor with a new modelling construct to provide support for structured types, which can be defined in terms of two new clauses: record declarations and record extensions. Both enable users to define their custom reusable types, that are treated underline by Rodin as Event-B constant sets and relations, supported by additional axioms, which the plug-in generates to simplify the proofs.

	=== Motivations ===		== Motivations ==

	Main reasons for implementing mathematical extensions are:		Main reasons for implementing mathematical extensions are:
Line 18:		Line 18:
	The motivation for development of Records plug-in was to fill the gap in Event-B language - a missing support of a syntax for the direct definition of structured types. Some of the industrial partners expressed a desire to have this missing feature in Event-B, that would allow them to define their own structured types such as records or classes. Theoretically these structures could be modelled with existing Event-B capabilities via projection functions. Backed up by a refined theoretical proposal Records plug-in was developed to extend the standard Event-B notation with requested capability.		The motivation for development of Records plug-in was to fill the gap in Event-B language - a missing support of a syntax for the direct definition of structured types. Some of the industrial partners expressed a desire to have this missing feature in Event-B, that would allow them to define their own structured types such as records or classes. Theoretically these structures could be modelled with existing Event-B capabilities via projection functions. Backed up by a refined theoretical proposal Records plug-in was developed to extend the standard Event-B notation with requested capability.

	=== Choices / Decisions ===		== Choices / Decisions ==

	On the Core Rodin Platform side, implementing mathematical extensions required to make some parts of the code extensible, that were not designed to be so, namely the lexer and the parser. We were using tools that automatically generated them from a fixed grammar description, so we had to change to other technologies. A [http://wiki.event-b.org/index.php/Constrained_Dynamic_Parser study] has been made on available technologies. The Pratt algorithm was selected for its adequation with the purpose and it did not have the drawbacks of other technologies:		On the Core Rodin Platform side, implementing mathematical extensions required to make some parts of the code extensible, that were not designed to be so, namely the lexer and the parser. We were using tools that automatically generated them from a fixed grammar description, so we had to change to other technologies. A [http://wiki.event-b.org/index.php/Constrained_Dynamic_Parser study] has been made on available technologies. The Pratt algorithm was selected for its adequation with the purpose and it did not have the drawbacks of other technologies:
Line 32:		Line 32:
	Records plug-in required the extension of the Rodin database with the new constructs to support structured types. On the other hand the Event-B language itself did not support extension at that time. For that reason the decision was made to address extensibility problem at the lowest level possible, which was Rodin database, but to model structured types using standard Event-B notation at the level below. The translation from extended to standard syntax has been entrusted to the static checker, that was also extended for this purpose. Thus the plug-in provides the users with notation for record declarations and extensions in unchecked models, but the checked versions operate with standard Event-B constructs.		Records plug-in required the extension of the Rodin database with the new constructs to support structured types. On the other hand the Event-B language itself did not support extension at that time. For that reason the decision was made to address extensibility problem at the lowest level possible, which was Rodin database, but to model structured types using standard Event-B notation at the level below. The translation from extended to standard syntax has been entrusted to the static checker, that was also extended for this purpose. Thus the plug-in provides the users with notation for record declarations and extensions in unchecked models, but the checked versions operate with standard Event-B constructs.

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

	* Pre-studies (states of the art, proposals, discussions).		* Pre-studies (states of the art, proposals, discussions).
Line 49:		Line 49:
	** [http://wiki.event-b.org/images/Theory_UM.pdf]		** [http://wiki.event-b.org/images/Theory_UM.pdf]

	=== Planning ===		== Planning ==
	The Theory plug-in v2.1 is released. Work will continue on general maintenance, bug fixes as well adding new features as requested by the users of the plug-in.		The Theory plug-in v2.1 is released. Work will continue on general maintenance, bug fixes as well adding new features as requested by the users of the plug-in.


	[[Category:D32 Deliverable]]		[[Category:D32 Deliverable]]

imported>Nicolas: /* Planning */

2010-11-30T15:38:17Z

Planning

← Older revision		Revision as of 15:38, 30 November 2010
Line 50:		Line 50:

	=== Planning ===		=== Planning ===
	The Theory plug-in v2.1 is released. Work will continue on general maintenance, bug fixes as well adding new ~~feature~~ as requested by the users of the plug-in.		The Theory plug-in v2.1 is released. Work will continue on general maintenance, bug fixes as well adding new features as requested by the users of the plug-in.

	~~This paragraph shall give a timeline and current status (as of 28 Jan 2011).~~

	~~{{TODO\|What will remain to do after Rodin 2.1 ?}}~~

	[[Category:D32 Deliverable]]		[[Category:D32 Deliverable]]

imported>Im06r: /* Planning */

2010-11-28T21:24:49Z

Planning

← Older revision		Revision as of 21:24, 28 November 2010
Line 50:		Line 50:

	=== Planning ===		=== Planning ===
			The Theory plug-in v2.1 is released. Work will continue on general maintenance, bug fixes as well adding new feature as requested by the users of the plug-in.

	This paragraph shall give a timeline and current status (as of 28 Jan 2011).		This paragraph shall give a timeline and current status (as of 28 Jan 2011).

imported>Im06r: /* Overview */

2010-11-28T21:19:46Z

Overview

← Older revision		Revision as of 21:19, 28 November 2010
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 ~~defining his own mathematical~~ operators, basic predicates and algebraic types. Along with these additional notations, the user can also define new proof rules (prover 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 (prover extensions).

	A theory is a file that can be used to define new algebraic types, new operators/predicates and new proof rules. Theories are developed in the Rodin workspace, and proof obligations are generated to validate prover and mathematical extensions. When a theory is completed and (optionally) validated, the user can make it available for use in models (this action is called the deployment of a theory). Theories are deployed to the current workspace (i.e., Workspace Scope), and the user can use any defined extensions in any project within the workspace.		A theory is a file that can be used to define new algebraic types, new operators/predicates and new proof rules. Theories are developed in the Rodin workspace, and proof obligations are generated to validate prover and mathematical extensions. When a theory is completed and (optionally) validated, the user can make it available for use in models (this action is called the deployment of a theory). Theories are deployed to the current workspace (i.e., Workspace Scope), and the user can use any defined extensions in any project within the workspace.

imported>Im06r: /* Choices / Decisions */

2010-11-28T21:17:03Z

Choices / Decisions

← Older revision		Revision as of 21:17, 28 November 2010
Line 28:		Line 28:
	Besides, we wanted to set up a way to publish and share theories for Rodin users, in order to constitute a database of pre-built theories for everyone to use and contribute. This has been realised by adding a new tracker on SourceForge site ([http://sourceforge.net/tracker/?group_id=108850&atid=1558661]).		Besides, we wanted to set up a way to publish and share theories for Rodin users, in order to constitute a database of pre-built theories for everyone to use and contribute. This has been realised by adding a new tracker on SourceForge site ([http://sourceforge.net/tracker/?group_id=108850&atid=1558661]).

	The Theory plug-in contributes a theory construct to the Rodin database. Theories were used in the Rule-based Prover (before it was discontinued) as a placeholder for rewrite rules. Given the usability advantages of the theory component, it was decided to use it to define mathematical extensions (new operators and new datatypes). Another advantage of using the theory construct is the possibility of using proof obligations to ensure soundness of the formalism is not compromised. Proof obligations are generated to validate any properties of new operators (e.g., associativity). With regards to prover extensions, it was decided that the Theory plug-in inherits the capabilities to define and validate rewrite rules from the Rule-based Prover. Furthermore, a simple yet powerful ~~way~~ of ~~defining~~ inference rules is added.		The Theory plug-in contributes a theory construct to the Rodin database. Theories were used in the Rule-based Prover (before it was discontinued) as a placeholder for rewrite rules. Given the usability advantages of the theory component, it was decided to use it to define mathematical extensions (new operators and new datatypes). Another advantage of using the theory construct is the possibility of using proof obligations to ensure that the soundness of the formalism is not compromised. Proof obligations are generated to validate any properties of new operators (e.g., associativity). With regards to prover extensions, it was decided that the Theory plug-in inherits the capabilities to define and validate rewrite rules from the Rule-based Prover. Furthermore, support for a simple yet powerful subset of inference rules is added, and polymorphic theorems can be defined within the same setting. Proof obligations are, again, used as a filter against potentially unsound proof rules.

	Records plug-in required the extension of the Rodin database with the new constructs to support structured types. On the other hand the Event-B language itself did not support extension at that time. For that reason the decision was made to address extensibility problem at the lowest level possible, which was Rodin database, but to model structured types using standard Event-B notation at the level below. The translation from extended to standard syntax has been entrusted to the static checker, that was also extended for this purpose. Thus the plug-in provides the users with notation for record declarations and extensions in unchecked models, but the checked versions operate with standard Event-B constructs.		Records plug-in required the extension of the Rodin database with the new constructs to support structured types. On the other hand the Event-B language itself did not support extension at that time. For that reason the decision was made to address extensibility problem at the lowest level possible, which was Rodin database, but to model structured types using standard Event-B notation at the level below. The translation from extended to standard syntax has been entrusted to the static checker, that was also extended for this purpose. Thus the plug-in provides the users with notation for record declarations and extensions in unchecked models, but the checked versions operate with standard Event-B constructs.

imported>Im06r: /* Choices / Decisions */

2010-11-28T21:07:33Z

Choices / Decisions

← Older revision		Revision as of 21:07, 28 November 2010
Line 27:		Line 27:

	Besides, we wanted to set up a way to publish and share theories for Rodin users, in order to constitute a database of pre-built theories for everyone to use and contribute. This has been realised by adding a new tracker on SourceForge site ([http://sourceforge.net/tracker/?group_id=108850&atid=1558661]).		Besides, we wanted to set up a way to publish and share theories for Rodin users, in order to constitute a database of pre-built theories for everyone to use and contribute. This has been realised by adding a new tracker on SourceForge site ([http://sourceforge.net/tracker/?group_id=108850&atid=1558661]).

			The Theory plug-in contributes a theory construct to the Rodin database. Theories were used in the Rule-based Prover (before it was discontinued) as a placeholder for rewrite rules. Given the usability advantages of the theory component, it was decided to use it to define mathematical extensions (new operators and new datatypes). Another advantage of using the theory construct is the possibility of using proof obligations to ensure soundness of the formalism is not compromised. Proof obligations are generated to validate any properties of new operators (e.g., associativity). With regards to prover extensions, it was decided that the Theory plug-in inherits the capabilities to define and validate rewrite rules from the Rule-based Prover. Furthermore, a simple yet powerful way of defining inference rules is added.

	Records plug-in required the extension of the Rodin database with the new constructs to support structured types. On the other hand the Event-B language itself did not support extension at that time. For that reason the decision was made to address extensibility problem at the lowest level possible, which was Rodin database, but to model structured types using standard Event-B notation at the level below. The translation from extended to standard syntax has been entrusted to the static checker, that was also extended for this purpose. Thus the plug-in provides the users with notation for record declarations and extensions in unchecked models, but the checked versions operate with standard Event-B constructs.		Records plug-in required the extension of the Rodin database with the new constructs to support structured types. On the other hand the Event-B language itself did not support extension at that time. For that reason the decision was made to address extensibility problem at the lowest level possible, which was Rodin database, but to model structured types using standard Event-B notation at the level below. The translation from extended to standard syntax has been entrusted to the static checker, that was also extended for this purpose. Thus the plug-in provides the users with notation for record declarations and extensions in unchecked models, but the checked versions operate with standard Event-B constructs.

← Older revision		Revision as of 13:04, 20 December 2010
Line 37:		Line 37:
	** [http://deploy-eprints.ecs.soton.ac.uk/216/ ''Proposals for Mathematical Extensions for Event-B'']		** [http://deploy-eprints.ecs.soton.ac.uk/216/ ''Proposals for Mathematical Extensions for Event-B'']
	** [http://deploy-eprints.ecs.soton.ac.uk/251/ ''Mathematical Extension in Event-B through the Rodin Theory Component'']		** [http://deploy-eprints.ecs.soton.ac.uk/251/ ''Mathematical Extension in Event-B through the Rodin Theory Component'']
	** [http://wiki.event-b.org/index.php/Constrained_Dynamic_Parser#Design_Alternatives]		** [http://wiki.event-b.org/index.php/Constrained_Dynamic_Parser#Design_Alternatives ''Generic Parser's Design Alternatives'' ]
	** [http://wiki.event-b.org/index.php/Structured_Types ''Theoretical Description of Structured Types'']		** [http://wiki.event-b.org/index.php/Structured_Types ''Theoretical Description of Structured Types'']
	* Technical details (specifications).		* Technical details (specifications).
	** [http://wiki.event-b.org/index.php/Mathematical_Extensions]		** [http://wiki.event-b.org/index.php/Mathematical_Extensions ''Mathematical_Extensions wiki page'']
	** [http://wiki.event-b.org/index.php/Constrained_Dynamic_Lexer]		** [http://wiki.event-b.org/index.php/Constrained_Dynamic_Lexer ''Constrained Dynamic Lexer wiki page'']
	** [http://wiki.event-b.org/index.php/Constrained_Dynamic_Parser]		** [http://wiki.event-b.org/index.php/Constrained_Dynamic_Parser ''Constrained Dynamic Parser wiki page'']
	** [http://wiki.event-b.org/index.php/Theory_Plug-in]		** [http://wiki.event-b.org/index.php/Theory_Plug-in ''Theory plug-in wiki page]
	** [http://wiki.event-b.org/index.php/Records_Extension ''Records Extension Documentation'']		** [http://wiki.event-b.org/index.php/Records_Extension ''Records Extension Documentation on wiki'']
	* Teaching materials (tutorials).		* Teaching materials (tutorials).
	* User's guides.		* User's guides.
	** [http://wiki.event-b.org/images/Theory_UM.pdf]		** [http://wiki.event-b.org/images/Theory_UM.pdf ''Theory Plug-in User Manual'']

	= Planning =		= Planning =