Rule-based Prover Plug-in: Difference between revisions
From Event-B
Jump to navigationJump to search
imported>Im06r |
imported>Im06r No edit summary |
||
| Line 1: | Line 1: | ||
This page provides extensive documentation for the rule-based prover plug-in. | This page provides extensive documentation for the rule-based prover plug-in. | ||
== News == | |||
* ''1st December 2009'': [[#Version_0.0.1|Version 0.0.1]] released. It is based on Rodin 1.1.0. | |||
== User Documentation == | == User Documentation == | ||
| Line 9: | Line 13: | ||
:[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.] | ||
== Releases == | == Releases == | ||
Revision as of 12:07, 1 December 2009
This page provides extensive documentation for the rule-based prover plug-in.
News
- 1st December 2009: Version 0.0.1 released. It is based on Rodin 1.1.0.
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.
Releases
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.
