Theory Plug-in

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, 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.

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.