Difference between revisions of "Theory Plug-in"
imported>Im06r |
imported>Im06r |
||
| (12 intermediate revisions by the same user not shown) | |||
| Line 1: | Line 1: | ||
Return to [[Rodin Plug-ins]] | Return to [[Rodin Plug-ins]] | ||
| + | |||
| + | See also [[Theory News and Support]] | ||
The Theory plug-in is the successor of the Rule-based Prover (which will be referred to as RbP) plug-in. The Theory plug-in | The Theory plug-in is the successor of the Rule-based Prover (which will be referred to as RbP) plug-in. The Theory plug-in | ||
provides capabilities to extend the Event-B language and the proving infrastructure in a familiar fashion to Rodin users. If you are looking for the user manual or the latest news on the Theory plug-in, please refer to [[Theory News and Support|Theory News and Support]]. | provides capabilities to extend the Event-B language and the proving infrastructure in a familiar fashion to Rodin users. If you are looking for the user manual or the latest news on the Theory plug-in, please refer to [[Theory News and Support|Theory News and Support]]. | ||
| − | This page provides useful information about the plug-in and its | + | This page provides useful information about the plug-in and its capabilities. |
===Motivation=== | ===Motivation=== | ||
| − | The mathematical language used in Event-B has so far been fixed in the Abstract Syntax Tree (AST). See [http://wiki.event-b.org/index.php/Event-B_Mathematical_Language Mathematical Language] for more details. However, in Rodin 2.0, support for customized operator has been introduced. | + | The mathematical language used in Event-B has so far been fixed in the Abstract Syntax Tree (AST). See [http://wiki.event-b.org/index.php/Event-B_Mathematical_Language Mathematical Language] for more details. However, in Rodin 2.0, support for customized operator has been introduced. See [http://wiki.event-b.org/index.php/Mathematical_extensions Mathematical Extensions]. |
Prior to Rodin 2.0, since the AST of Event-B mathematical language was fixed, it was not possible to defined reusable polymorphic operators and datatypes. A workaround was to define any required operators as set constructs in contexts. Originally, contexts were supposed to provide a parametrization of machines. The aforementioned limitations of the AST lead to users to use contexts for purposes for which they were not intentionally devised. Examples of operators that can be useful to users include the sequence operator and the bag operator. | Prior to Rodin 2.0, since the AST of Event-B mathematical language was fixed, it was not possible to defined reusable polymorphic operators and datatypes. A workaround was to define any required operators as set constructs in contexts. Originally, contexts were supposed to provide a parametrization of machines. The aforementioned limitations of the AST lead to users to use contexts for purposes for which they were not intentionally devised. Examples of operators that can be useful to users include the sequence operator and the bag operator. | ||
| Line 14: | Line 16: | ||
Mathematical extensions are new operator definitions and new datatype definitions. Operator definitions can be expression operators (card) and predicate operators (finite). Datatypes extensions can be used to define enumerated datatypes (DIRECTION) as well as inductive datatypes (Tree). | Mathematical extensions are new operator definitions and new datatype definitions. Operator definitions can be expression operators (card) and predicate operators (finite). Datatypes extensions can be used to define enumerated datatypes (DIRECTION) as well as inductive datatypes (Tree). | ||
| − | The placeholder for mathematical and prover extensions is a Theory construct which looks similar to contexts and machines. A theory can include datatypes definitions, operator definitions, inference and rewrite rules. | + | The placeholder for mathematical and prover extensions is a Theory construct which looks similar to contexts and machines. A theory can include datatypes definitions, operator definitions, inference and rewrite rules. The user manual provides a step-by-step guide to developing and using theories. |
===Capabilities=== | ===Capabilities=== | ||
| + | The Theory plug-in has the following capabilities: | ||
| + | * Theory Definition | ||
| + | ** Definition of datatypes: datatypes are defined by supplying the types on which they are polymorphic, a set of constructors one of which has to be a base constructor. Each constructor may or may not have destructors. | ||
| + | ** Definition of operators: operators can be defined as predicate or expression operators. An expression operator is an operator that "returns" an expression, an example existing operator is ''card(s)''. A predicate operator is one that "returns" a predicate, an example existing predicate operator is ''finite(s)''. | ||
| + | ** Definition of rewrite rules: rewrite rules are one-directional equalities that can be applied from left to right. The Theory plug-in can be used to define rewrite rules. | ||
| + | ** Definition of inference rules: inference rules can be used to infer new hypotheses, split a goal into sub-goals or discharge sequents. | ||
| + | ** Validation of extensions: where appropriate, proof obligations are generated to ensure soundness of extensions. This includes, proof obligations for validity of inference and rewrite rules, as well as proof obligations to validate operator properties such as associativity and commutativity. | ||
| + | * Theory Deployment: this step signifies that a theory is ready for use. | ||
| + | ** Theories can be deployed after they have been optionally validated by the user. It is strongly advisable to discharge all proof obligations before deployment. | ||
| + | ** Once a theory has been deployed to the designated project (at the moment MathExtensions project), all its extensions (mathematical and prover extensions) can be used in models as well as other theories. | ||
===Insider Look=== | ===Insider Look=== | ||
| + | The Theory plug-in partially satisfies the requirements outlined in the following document: | ||
| + | * [http://deploy-eprints.ecs.soton.ac.uk/80/ Abrial, Jean-Raymond and Butler, Michael and Schmalz, Matthias and Hallerstede, Stefan and Voisin, Laurent. Mathematical Extensions Proposal] | ||
| + | |||
| + | A more accurate description of the implemented plug-in can be found in the following document: | ||
| + | * [http://deploy-eprints.ecs.soton.ac.uk/251/ Mathematical Extensions Summary] | ||
| + | |||
| + | The following two papers describe rewriting and well-definedness issues that has to be accounted for: | ||
| − | + | * [http://eprints.ecs.soton.ac.uk/18269/ Issam Maamria, Michael Butler, Andrew Edmunds, and Abdolbaghi Rezazadeh. On an Extensible Rule-based Prover for Event-B, ABZ'2010.] | |
| − | + | * [http://eprints.ecs.soton.ac.uk/21221/ Issam Maamria, Michael Butler. Rewriting and Well-Definedness within a Proof System.] | |
===Improvements and Bugs=== | ===Improvements and Bugs=== | ||
| − | See also the late [[Rule-based Prover Plug-in]], the last release of | + | See also the late [[Rule-based Prover Plug-in]], the last release of which was v0.3. The Theory plug-in starts at version v0.5. |
Revision as of 13:25, 27 October 2010
Return to Rodin Plug-ins
See also Theory News and Support
The Theory plug-in is the successor of the Rule-based Prover (which will be referred to as RbP) plug-in. The Theory plug-in provides capabilities to extend the Event-B language and the proving infrastructure in a familiar fashion to Rodin users. If you are looking for the user manual or the latest news on the Theory plug-in, please refer to Theory News and Support. This page provides useful information about the plug-in and its capabilities.
Motivation
The mathematical language used in Event-B has so far been fixed in the Abstract Syntax Tree (AST). See Mathematical Language for more details. However, in Rodin 2.0, support for customized operator has been introduced. See Mathematical Extensions.
Prior to Rodin 2.0, since the AST of Event-B mathematical language was fixed, it was not possible to defined reusable polymorphic operators and datatypes. A workaround was to define any required operators as set constructs in contexts. Originally, contexts were supposed to provide a parametrization of machines. The aforementioned limitations of the AST lead to users to use contexts for purposes for which they were not intentionally devised. Examples of operators that can be useful to users include the sequence operator and the bag operator.
Overview
The Theory plug-in is a Rodin extension that provides the facility to define mathematical extensions as well as prover extensions. Mathematical extensions are new operator definitions and new datatype definitions. Operator definitions can be expression operators (card) and predicate operators (finite). Datatypes extensions can be used to define enumerated datatypes (DIRECTION) as well as inductive datatypes (Tree).
The placeholder for mathematical and prover extensions is a Theory construct which looks similar to contexts and machines. A theory can include datatypes definitions, operator definitions, inference and rewrite rules. The user manual provides a step-by-step guide to developing and using theories.
Capabilities
The Theory plug-in has the following capabilities:
- Theory Definition
- Definition of datatypes: datatypes are defined by supplying the types on which they are polymorphic, a set of constructors one of which has to be a base constructor. Each constructor may or may not have destructors.
- Definition of operators: operators can be defined as predicate or expression operators. An expression operator is an operator that "returns" an expression, an example existing operator is card(s). A predicate operator is one that "returns" a predicate, an example existing predicate operator is finite(s).
- Definition of rewrite rules: rewrite rules are one-directional equalities that can be applied from left to right. The Theory plug-in can be used to define rewrite rules.
- Definition of inference rules: inference rules can be used to infer new hypotheses, split a goal into sub-goals or discharge sequents.
- Validation of extensions: where appropriate, proof obligations are generated to ensure soundness of extensions. This includes, proof obligations for validity of inference and rewrite rules, as well as proof obligations to validate operator properties such as associativity and commutativity.
- Theory Deployment: this step signifies that a theory is ready for use.
- Theories can be deployed after they have been optionally validated by the user. It is strongly advisable to discharge all proof obligations before deployment.
- Once a theory has been deployed to the designated project (at the moment MathExtensions project), all its extensions (mathematical and prover extensions) can be used in models as well as other theories.
Insider Look
The Theory plug-in partially satisfies the requirements outlined in the following document:
A more accurate description of the implemented plug-in can be found in the following document:
The following two papers describe rewriting and well-definedness issues that has to be accounted for:
- Issam Maamria, Michael Butler, Andrew Edmunds, and Abdolbaghi Rezazadeh. On an Extensible Rule-based Prover for Event-B, ABZ'2010.
- Issam Maamria, Michael Butler. Rewriting and Well-Definedness within a Proof System.
Improvements and Bugs
See also the late Rule-based Prover Plug-in, the last release of which was v0.3. The Theory plug-in starts at version v0.5.
