Modularisation Plug-in Composition Semantics

From Event-B
Jump to navigationJump to search
The printable version is no longer supported and may have rendering errors. Please update your browser bookmarks and please use the default browser print function instead.

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 2: Atomicity Refinement