Modularisation Integration Issues: Difference between revisions
imported>Alexili mNo edit summary |
imported>Alexili mNo edit summary |
||
| Line 1: | Line 1: | ||
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. | 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 | 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 === | ===Core Platform integration === | ||
Revision as of 11:15, 6 September 2010
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.
