Modularisation Integration Issues - Revision history

imported>Alexili at 11:34, 6 September 2010

2010-09-06T11:34:49Z

← Older revision		Revision as of 11:34, 6 September 2010
Line 5:		Line 5:
	===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.		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 ===		=== 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 ===		=== 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 ===		=== 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.

imported>Alexili at 11:21, 6 September 2010

2010-09-06T11:21:31Z

← Older revision		Revision as of 11:21, 6 September 2010
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 ===

imported>Alexili at 11:15, 6 September 2010

2010-09-06T11:15:08Z

← Older revision		Revision as of 11:15, 6 September 2010
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 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.		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 ===

imported>Alexili at 11:14, 6 September 2010

2010-09-06T11:14:13Z

← Older revision		Revision as of 11:14, 6 September 2010
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 ~~operation~~ 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 in 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 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.		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.

imported>Alexili at 11:13, 6 September 2010

2010-09-06T11:13:18Z

← Older revision		Revision as of 11:13, 6 September 2010
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 operation 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 in 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 operation 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 in 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 is used a lingua franca for plugins extending the core ~~languages~~ and also 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.		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.

	===		===Core Platform integration ===

			=== Text editor integration ===

			=== ProB integration ===

			=== Documentation plugin integration ===

imported>Alexili: New page: 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 ...

2010-09-06T11:11:09Z

New page: 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 ...

New page

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 operation 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 in 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 is used a lingua franca for plugins extending the core languages and also 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.

===