imported>WikiSysop |
imported>Andy |
Line 1: |
Line 1: |
− | == Introduction ==
| + | TODO - some description of the use of Theories in CG |
− | | |
− | 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_Workshop_2009 | 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
| |
Revision as of 07:51, 15 May 2012
TODO - some description of the use of Theories in CG