Difference between revisions of "Rule-based Prover Plug-in"
From Event-B
Jump to navigationJump to searchimported>Im06r (→News) |
imported>Im06r |
||
| Line 10: | Line 10: | ||
''1st December 2009'' | ''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 dischareg or reviewed". | ||
| + | * It is expected that Associative and Associative Commutative matching will have some issues. These will get rectified in the next release. | ||
Revision as of 11:58, 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.
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 dischareg or reviewed".
- It is expected that Associative and Associative Commutative matching will have some issues. These will get rectified in the next release.
