The Rodin Workshop 2009 Wishlist
The following list has been established during the Rodin User and Developer Workshop 2009 (July 15-17 2009):
- Enabledness POs
- Automatic refinement
- Support for probability
- Automated provers / SMT for set theory
- common context
- used hypothesis
- extensible operator
- Reasoned modeling support
- Flexible document management
Structural Checker Plug-in
The idea of such a plug-in is to perform structural checks on Event-B models.
It could for example ensure that some good-usage rules are enforced, or produce a list of warnings to provide help when modeling (eg. an anticipated event has been found in last refinement).
- Support for re-play of proofs on other POs