Difference between pages "Plug-in Wishlist" and "The Use of Theories in Code Generation"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>WikiSysop
 
imported>Andy
(New page: TODO - some description of the use of Theories in CG)
 
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