Difference between revisions of "Modularisation Plug-in Composition Semantics"
From Event-B
Jump to navigationJump to searchimported>Alexili (New page: {{TODO|This is an internal draft document}} ==Approach 1: Reducing to A-style== ==Approach 2: Atomicity Refinement==) |
imported>Mathieu m (Category:Plugin) |
||
| (One intermediate revision by one other user not shown) | |||
| Line 1: | Line 1: | ||
{{TODO|This is an internal draft document}} | {{TODO|This is an internal draft document}} | ||
| + | |||
| + | ==The meaning of module composition== | ||
| + | |||
| + | This page explains what it means to import a module and rely on the interface operations implemented by the module. In particular, how one can, at least in principle, construct a single flat Event-B machine from a specification where a final refinement step and its abstraction rely on modules. This serves two purposes: it gives exact characterisation of the behaviour of a modular specification; it serves as a reference for implementation-stage composition strategies. | ||
| + | |||
==Approach 1: Reducing to A-style== | ==Approach 1: Reducing to A-style== | ||
==Approach 2: Atomicity Refinement== | ==Approach 2: Atomicity Refinement== | ||
| + | |||
| + | [[Category:Plugin]] | ||
Latest revision as of 20:58, 10 November 2009
TODO: This is an internal draft document
The meaning of module composition
This page explains what it means to import a module and rely on the interface operations implemented by the module. In particular, how one can, at least in principle, construct a single flat Event-B machine from a specification where a final refinement step and its abstraction rely on modules. This serves two purposes: it gives exact characterisation of the behaviour of a modular specification; it serves as a reference for implementation-stage composition strategies.
