Modularisation Integration Issues: Difference between revisions
imported>Alexili mNo edit summary |
imported>Alexili mNo edit summary |
||
| Line 4: | Line 4: | ||
===Core Platform integration === | ===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 of inserting a new module (a rule container) in between the existing rules. One example where this is needed is a kind of 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 === | === Text editor integration === | ||
Revision as of 11:21, 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.
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 of inserting a new module (a rule container) in between the existing rules. One example where this is needed is a kind of 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.
