Difference between revisions of "Theory Plug-in"
imported>Im06r |
imported>Im06r |
||
| Line 7: | Line 7: | ||
===Motivation=== | ===Motivation=== | ||
The mathematical language used in Event-B has so far been fixed in the 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 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. | ||
| − | Prior to Rodin 2.0, the Abstract Syntax Tree of Event-B mathematical language was fixed | + | |
| + | Prior to Rodin 2.0, since the Abstract Syntax Tree 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=== | ===Overview=== | ||
Revision as of 12:25, 27 October 2010
Return to Rodin Plug-ins
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 design.
Motivation
The mathematical language used in Event-B has so far been fixed in the AST. See Mathematical Language for more details. However, in Rodin 2.0, support for customized operator has been introduced.
Prior to Rodin 2.0, since the Abstract Syntax Tree 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
Capabilities
Insider Look
- 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 the which was v0.3. The Theory plug-in starts at version v0.5.
