Modularisation Integration Issues

From Event-B
Revision as of 11:15, 6 September 2010 by imported>Alexili
Jump to navigationJump to search

The Modularisation plugin extends Event-B notation with the notions of interface and operation call. An interface is a new component kind declaring some external variables, invariants and operations. A machine may import an interface component and use operations in action expressions. A machine may also implement an interface, that is, give a more detailed description of how interface operations are to be realised. All these new concepts necessitate an extension of the input notation. Crucially, the extensions are only present in the in the unchecked versions of components (unchecked interface, unchecked machine). Statically checked components are generated to be plain Event-B.

As a general direction, we propose that statically checked machines (an interface component is translated into a statically checked machine as well) and contexts are used as a lingua franca for plugins extending the core language and also for the plugins analysing and manipulating models. There should be no logical difficulties as a statically checked component contains a superset of the information available from an unchecked component. Some attributes are not embedded in a statically checked component but can be located by navigating to the element source.

Core Platform integration

Text editor integration

ProB integration

Documentation plugin integration