Theory Plug-in: Difference between revisions

From Event-B
Jump to navigationJump to search
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. As such, 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 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.