Difference between revisions of "Plug-in Wishlist"

From Event-B
Jump to navigationJump to search
imported>Pascal
 
imported>Pascal
(No difference)

Revision as of 14:35, 2 October 2009

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).