Difference between revisions of "Modularisation Plug-in Composition Semantics"

From Event-B
Jump to navigationJump to search
imported>Alexili
imported>Mathieu
 
Line 8: Line 8:
  
 
==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.

Approach 1: Reducing to A-style

Approach 2: Atomicity Refinement