Difference between revisions of "Theory Plug-in"
imported>Im06r |
imported>Im06r |
||
| Line 11: | Line 11: | ||
===Overview=== | ===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. In this user manual, we provide a step-by-step guide to developing and using theories. | ||
===Capabilities=== | ===Capabilities=== | ||
Revision as of 12:26, 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 Abstract Syntax Tree (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 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. In this user manual, we provide a step-by-step guide to developing and using theories.
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.
