Plug-in Wishlist
From Event-B
Jump to navigationJump to search
Introduction
This page has been created to give a wish list of tool plug-ins that cannot be resourced by Deploy. These plug-ins could be developed by Deploy partners or by external partners.
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).
Other items
- Support for re-play of proofs on other POs.
