Modularisation Integration Issues

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

There are no pressing issues regarding the platform integration, however, for the long-term maintainability it would help if the Plaltform provided a more flexible approach to extending component configurations (a configuration is a set of static checking and proof generation rules). Currently one can add new bag of rules alongside an existing configuration or extend an configuration by adding new rules. There is, however, a major limitation in the way a configuration is extended: there is no provision for inserting a new module (a rule container) in between the existing rules. One example where this is needed is a rule that imports new declarations and makes them available to other rules. The current solution in the plugin is to copy all the static checking modules and, without changing them, rearrange into a new configuration. A better solution would be a before attribute alongside with the existing prereq attribute of a module declaration.

Text editor integration

Until an extension facility for the editor is defined it would help to have a fixed and well defined set of rules for submitting a text editor extension request. Currently, it is unclear how to approach this issue.

ProB integration

At the moment, the modularisation plugin is not compatible with ProB. An initial investigation suggests that ProB navigates to unchecked contexts from a statically checked machine component. The modularisation plugin generates embedded context that do not correspond to any actual context components and hence ProB aborts failing to locate an unchecked context during the translation stage. The way forward would be to exchange the information on the inner working of ProB and the modularisation plugin and find a way to make statically checked machines produced by the plugin suitable for an input to ProB.

Documentation plugin integration

The documentation plugin unfortunately does not define any extension points. Ideally, it should follow the approach taken in the new pretty-printer realisation and allow plugin developers to contribute latex generation rules for their new elements.