Rule-based Prover Plug-in: Difference between revisions
From Event-B
Jump to navigationJump to search
imported>Im06r |
imported>Im06r |
||
| (8 intermediate revisions by the same user not shown) | |||
| Line 2: | Line 2: | ||
== News == | == News == | ||
* ''9th July 2010'': [[#Version_0.3.0|Version 0.3.0]] released. It is based on Rodin 1.3.1. | |||
* ''8th February 2010'': [[#Version_0.2.0|Version 0.2.0]] released. It is based on Rodin 1.2.0. | |||
* ''1st December 2009'': [[#Version_0.0.1|Version 0.0.1]] released. It is based on Rodin 1.1.0. | * ''1st December 2009'': [[#Version_0.0.1|Version 0.0.1]] released. It is based on Rodin 1.1.0. | ||
| Line 11: | Line 12: | ||
== User Documentation == | == User Documentation == | ||
The user manual is available | The user manual is available [http://wiki.event-b.org/images/Theory_User_Manual.pdf here]. | ||
== Other Documentation == | == Other Documentation == | ||
| Line 17: | Line 18: | ||
:[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/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/18273/ Issam Maamria, Michael Butler, Andrew Edmunds, and Abdolbaghi Rezazadeh. On an Extensible Rule-based Prover for Event-B, Technical Report.] | :[http://eprints.ecs.soton.ac.uk/18273/ Issam Maamria, Michael Butler, Andrew Edmunds, and Abdolbaghi Rezazadeh. On an Extensible Rule-based Prover for Event-B, Technical Report.] | ||
== Bugs & Problems == | |||
== Releases == | == Releases == | ||
===== Version 0.3.0 ===== | |||
''9th July 2010'' | |||
This release includes bug fixes, UI improvements, support for predicate variables. (TODO more docs) | |||
===== Version 0.2.0 ===== | |||
''8th February 2010'' | |||
This release includes bug fixes, and added (partial) support for rules containing set extension (singleton). | |||
===== Version 0.0.1 ===== | ===== Version 0.0.1 ===== | ||
Latest revision as of 17:11, 9 July 2010
This page provides extensive documentation for the rule-based prover plug-in.
News
- 9th July 2010: Version 0.3.0 released. It is based on Rodin 1.3.1.
- 8th February 2010: Version 0.2.0 released. It is based on Rodin 1.2.0.
- 1st December 2009: Version 0.0.1 released. It is based on Rodin 1.1.0.
Installation & Update
The installation or update for the theory/rule-based prover plug-in is available under the main Rodin Update site (http://rodin-b-sharp.sourceforge.net/updates). Like always, after the installation, restarting Rodin is recommended.
User Documentation
The user manual is available here.
Other Documentation
- Issam Maamria, Michael Butler, Andrew Edmunds, and Abdolbaghi Rezazadeh. On an Extensible Rule-based Prover for Event-B, ABZ'2010.
- Issam Maamria, Michael Butler, Andrew Edmunds, and Abdolbaghi Rezazadeh. On an Extensible Rule-based Prover for Event-B, Technical Report.
Bugs & Problems
Releases
Version 0.3.0
9th July 2010
This release includes bug fixes, UI improvements, support for predicate variables. (TODO more docs)
Version 0.2.0
8th February 2010
This release includes bug fixes, and added (partial) support for rules containing set extension (singleton).
Version 0.0.1
1st December 2009
This is the first public release of the Rule-based Prover plug-in (another name for this plug-in is Theory).
General:
- A theory construct is implemented to facilitate the specification and validation of rewrite rules.
- A pattern matching mechanism is implemented to check for applicability of rules as well as apply them.
- This is the first public release, so likely to have bugs. Use with care.
- Once rules are specified, only the validated ones are available. By validated, we mean "whose proof obligations are either dischared or reviewed".
- It is expected that Associative and Associative Commutative matching will have some issues. These will get rectified in the next release.
Limitations:
- This plug-in does not handle rules where the left hand side has a set extension.
- This plug-in should not be used to define rules with side conditions.
- Both these limitations will be addressed in future releases.
