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 of available from an unchecked component. Some attributes that are not embedded in a statically checked component but can be located by navigating to the element source.