has to occur

Building Specifications in the Event-B Institution]
Building Specifications in the Event-B Institution

M. Farrell]Marie Farrell
Department of Computer Science, Maynooth University, Ireland
This work was initially funded by a Government of Ireland Postgraduate Grant from the Irish Research Council, and subsequently supported by EPSRC Hubs for Robotics and AI in Hazardous Environments: EP/R026092 (FAIR-SPACE)

R. Monahan]Rosemary Monahan
Department of Computer Science, Maynooth University, Ireland

J.F. Power]James F. Power
Department of Computer Science, Maynooth University, Ireland

This paper describes a formal semantics for the Event-B specification
language using the theory of institutions.  We define an institution for
Event-B, , and prove that it meets the validity requirements
for satisfaction preservation and model amalgamation.  We also present a
series of functions that show how the constructs of the Event-B
specification language can be mapped into our institution.  Our
semantics sheds new light on the structure of the Event-B language,
allowing us to clearly delineate three constituent sub-languages: the
superstructure, infrastructure and mathematical languages.  One of the
principal goals of our semantics is to provide access to the generic
modularisation constructs available in institutions, including
specification-building operators for parameterisation and refinement.
We demonstrate how these features subsume and enhance the corresponding
features already present in Event-B through a detailed study of their use in a
worked example.  We have implemented our approach via a parser and
translator for Event-B specifications, , which also provides a
gateway to the  toolkit for heterogeneous specification.

§ INTRODUCTION

When formal methods are used in software development, formal specification languages are used to model software systems and to provide a basis for their verification. Event-B is an industrial-strength formal specification language that  originally evolved from the B-Method [59], and has been used in a multitude of domains including air-traffic control systems and medical devices [2]. Even though it is a mature formal specification language, Event-B has a number of drawbacks, particularly its lack of standardised modularisation constructs. In addition, while Event-B has been provided with a semantics in terms of proof obligations, the abstractness of this approach can make it difficult to deal formally with modularisation, or to provide a concrete basis for interoperability with other formalisms.

In this paper, we describe the formal constructions that allow the Event-B language to be embedded into the theory of institutions. Institutions are mathematical structures that make use of category theory and provide a generic framework for formalising a language or logic [23, 56].   Having built an institution to support the core concepts in Event-B, we can then use this institution as a target for the semantics of the full Event-B specification language.  This in turn gives access to a range of generic modularisation constructs and provides a foundation for interoperability between Event-B and other formalisms.

§.§ The structure of this paper

Sections <ref> and <ref> review the background material and basic definitions used in this paper.
The semantics of programming languages is a well-understood concept that has been studied for many years and we use it as a starting point for our research. It has become evident from our investigations that defining a semantics of a specification language, such as Event-B in our case, is a slightly different endeavour.
We provide some background on the semantics of specification languages in Section <ref>, and we give the basic definitions from the theory of institutions in this context.
In Section <ref> we give an overview of the Event-B specification language, describe its abstract syntax and introduce an example that we will use throughout the paper.

The core of our semantics is presented in Sections <ref> and
<ref>.  In Section <ref> we define our
institution for Event-B, , that was originally developed in
our previous work [18].

institution provides the mathematical structures that will act as a target
for the semantics of constructs from the Event-B language.

In Section <ref> we present a series of definitions of the  functions that map the abstract syntax of the Event-B language into the corresponding constructs in the  institution.  A key step here is
splitting the Event-B language into a three-layer model, by decomposing it into its superstructure, infrastructure and mathematical sub-languages.  As well as aiding the presentation, this also helps to expose the important features of the Event-B language.  In particular, once we have delineated these sub-languages, we can then employ the specification-building operators made available to us in the theory of institutions in our definition.

In the final sections of our paper, Sections <ref> and <ref>, we explore some of the consequences of our semantics.
We have validated our semantics by building a Haskell translator tool that we call , and in Section <ref> we describe the correspondence between this tool and our semantics. To illustrate the use of this tool in practice we apply it to our running example from Section <ref>.

Formal refinement is core to the Event-B development process and, as such, any formalisation of Event-B should take this into account. In Section <ref> we discuss what refinement means in the theory of institutions and show how our formalisation of  supports Event-B refinement.  Again, this is illustrated via our running example. The weaknesses that Event-B has in terms of modularisation are also addressed in Section <ref> where we show how the generic specification-building operators from the theory of institutions can provide a set of well-defined modularisation constructs for Event-B.

One of the major benefits of these operators is that they are designed to be used in an institution-, and thus formalism-independent fashion. In this way, we provide scope for interoperability between Event-B and other formalisms that have been incorporated into the institution-theoretic framework. Our semantics and its associated  tool are instrumental to this, since they allow us to bridge the gap between the  tool for Event-B and the  tool-set used for institutions.

§.§ Contributions of this paper

The principal contributions of this paper are summarised as follows:

* A formal semantics for the Event-B formal specification
language, defined as a series of functions from Event-B constructs
to specifications over .  This provides clarity on the
meaning of the language elements and their interaction, and allows
us to distinguish their differing levels of responsibility using the
three-layer model presented in Figure <ref>.

* A well-defined set of modularisation constructs using the
specification-building operators available through the theory of
institutions.  These are built-in to our semantics, they subsume and
extend the existing Event-B modularisation constructs, and they
provide a standardised approach to exploring new modularisation

* An explication of Event-B refinement in the context of the
institution.  Refinement in  incorporates and extends
the refinement constructs of Event-B, and our semantics provides a
more general context for exploring other options.

In addition, we have implemented an  translator tool that transforms
Event-B specifications that have been developed using the
Platform into specifications over the  institution.  We have
used this to validate our semantic definitions, and to provide
interoperability with the existing large corpus of specifications
available in this format [19].

§ THE SEMANTICS OF SPECIFICATION LANGUAGES

The study of the semantics of specification languages is closely
related to the semantics of programming languages, since both are
species of formal languages and, in many cases, have closely-related
origins.  For example, the specification language at the heart of the
Vienna Development Method (VDM) emerged from a line of research on the
semantics of programming languages starting with PL/1 and Algol
[37, 5].  Providing a
semantics has many practical advantages, since the semantics can
facilitate an increased understanding of the language, can provide a
basis for standardisation documents (e.g. the ISO standard for Z
[36]), can act as a specification for tools that
process the language, and can provide a basis for comparison and
interoperability with similar languages.

There are many approaches to defining a semantics for a
programming language, including denotational, operational and axiomatic
approaches among others
[69, 27, 70, 24].
A denotational semantics shows how to map the language constructs to
mathematical structures
[61, 58], and much of the
focus of this approach is on the correct selection of these
structures.  In contrast, the axiomatic approach characterises the
language in terms of the logical properties that must hold
[32], and much of the focus here is on proof
obligations and theorem-proving.  While not exclusive, these perspectives can often be reflected in the specification language itself, with a contrast between model-oriented and property-oriented approaches [9].

Some of the best-known model-oriented specification languages are Z
and VDM, both of which use typed-first order logic and set theory
overlaid with a set of language constructs to build specification units.
The Z specification language has been given a denotational semantics
by Spivey [66].  This semantics defines a
mapping from the basic syntactic unit of specification, a schema, to a
variety, which consists of a signature and set of models.  These models
map names used in the specification to appropriate values from the
underlying logic, such as sets, relations and functions.
In a similar vein, the semantics of VDM presented by Larsen and
Pawlowski [40] shows how to map a document to a
set of environments that model it; these environments map names to
their denotations.

In order to specify the behaviour of software systems, many specification languages are based on models that include a concept of state.
This has some similarity to the operational semantics used for programming
languages [30], though the overall approach is still essentially denotational.
An early example was the COLD specification language, and its semantics mapped the basic unit of specification, a class description, to a set of states along with a transition relation for each procedure [20].  The COLD specification-building operators are based on a class algebra, closely related to the structuring operators found in algebraic specification.  There are now many formalisms and languages which have semantics defined in terms of states and transitions including, for example, sequences of events in Object-Z [65, 64], the trace-based semantics of CSP [33, 54] and the behaviours of TLA+ [39, 42].

Along a similar vein, Unified Theories of
Programming (UTP) is a framework where specifications are interpreted
in terms of relations between their before and after states
[34]. This work, which is rooted in lattice theory,
somewhat parallels the approach using institutions, which is rooted in
category theory. More recent work uses UTP to define an algebra of programs and an associated refinement relation to derive denotational and operational models of the Guarded Command Language (GCL) and CSP [29].

Translational approaches to formal semantics appear throughout the literature, in particular, the denotational UTP semantics for Circus (combination of CSP and Z) which translates the CSP component of the specification into Z [48]. Another related translational approach is the semantics of a Dafny program which is given in terms of its translation to the Boogie intermediate verification language which generates the verification conditions to be proven with the Z3 SMT solver[41].

The semantics of Clear, the first algebraic specification language, is a mix of denotational semantics and category-theoretic elements [11]. Subsequently, the Common Algebraic Specification Language, CASL, was devised as a basis for future work on algebraic specifications using the unifying framework supplied by the theory of institutions [47]. The semantics of CASL follows a similar appooach to Clear and is thus founded in the theory of institutions. In particular, CASL's two step semantics involves translating CASL constructs to their underlying mathematical concepts. In this way, the CASL static semantics determines signatures and its model semantics determines model-classes over the underlying institution. The Heterogeneous Toolset, Hets, provides tool support for CASL specifications and facilitates the use of heterogeneous specifications in an institution-theoretic fashion [46].

§.§ Modularisation of specifications

In his semantics for Z, Spivey notes that while ordinary mathematical reasoning is similar to
software specification, the latter has the additional problem of
scale.  In this context, dealing with modularisation, including naming
and structuring constructs, assumes increased importance.  In modular software engineering, a system is decomposed into multiple independent modules that can be recomposed at a later stage to form the entire system [21]. There are a multitude of benefits to this approach including an ease of code maintenance, code reuse and enabling multiple engineers to work on different components of the same system in parallel.

In general, formal specification languages utilise refinement as their main modularisation technique with support for other modularisation features typically added after the language has been defined [15, 38].
The Z
specification language has a schema calculus, whose structuring operations are deliberately designed to look like logical operators, but this does not have to be the case.
One of the purposes of re-engineering the Z specification language in the development of Object-Z was to enhance the support for modular developments [71, 65]. Similarly, the VVSL language was developed as an approach to modularisation for VDM [43].

When Burstall and Goguen presented the
semantics of the Clear specification language
[11], one of their key observations was that
the specification-building operators could be given a meaning in a
very abstract way, almost independently of the notions of the
underlying formalism.  They characterised the meaning of a
Clear specification as an inter-connected collection of theories, where a theory is a closed set of properties derivable from the sentences of the specification.  In this context, the semantics of the
specification-structuring operators become theory transformations,
which Burstall and Goguen describe as “the mathematical essence of
Clear semantics”.

The Clear specification language shares many concepts with other
algebraic specification languages [8, 15], most
notably culminating in the Common Algebraic Specification Language
(CASL) [47] and the Heterogeneous Tool Set () [46].
These ideas were generalised in the theory of institutions, which describes these features in terms of category theory [23]. It has been observed that most of the formal languages used in Computer Science can be captured as institutions. One notable example is a category-theoretic formalisation of Z and its structuring mechanisms which captures the structure of modular Z specifications in a natural way [13].
The semantics of Event-B that we present
in this paper follows a similar school of thought by
first defining an institution for Event-B, called , in Section <ref>
and then translating Event-B specifications
into structured specifications in the  institution in Section <ref>.

§.§ Institutions: basic definitions

The theory of institutions, originally developed by Goguen and Burstall in a series of papers originating from their work on algebraic specification, provides a general framework for defining a logical system [22, 10, 23].  Institutions are generally used for representing logics in terms of their vocabulary (signatures), syntax (sentences) and semantics (models and satisfaction condition). The basic maxim of institutions, inspired by Tarski's theory of truth [67], is that

“Truth is invariant under change of notation”.

The use of institutions facilitates the development of specification language concepts, such as structuring of specifications, parameterisation, and refinement. This is achieved independently of the underlying logical system resulting in an environment for heterogeneous specification and combination of logics [55, 10].
The theory of institutions is rooted in category theory and our work follows the notation and terminology used by Sannella and Tarlecki [56]. Thus, we define
an institution as follows [23]:

An institution $\mathcal{INS}$ for some given logic consists of

* A category $\mathbf{Sign}_{\mathcal{INS}}$ whose objects are called signatures and  whose arrows are called signature morphisms.

* A functor $\mathbf{Sen}_{\mathcal{INS}}: \mathbf{Sign}_{\mathcal{INS}} \rightarrow \mathbf{Set}$ yielding a set $\mathbf{Sen}_{\mathcal{INS}}(\Sigma)$ of $\Sigma$-sentences for each signature $\Sigma \in \lvert \mathbf{Sign}_{\mathcal{INS}}\rvert$ and a function $\mathbf{Sen}_{\mathcal{INS}}(\sigma): \mathbf{Sen}_{\mathcal{INS}}(\Sigma)\rightarrow \mathbf{Sen}_{\mathcal{INS}}(\Sigma ')$ for each signature morphism
$\sigma: \Sigma \rightarrow \Sigma'$.

* A functor $\mathbf{Mod}_{\mathcal{INS}}: \mathbf{Sign}_{\mathcal{INS}}^{op} \rightarrow \mathbf{Cat}$ yielding a category $\mathbf{Mod}_{\mathcal{INS}}(\Sigma)$ of $\Sigma$-models for each signature $\Sigma\in\lvert \mathbf{Sign}_{\mathcal{INS}}\rvert$ and a functor $\mathbf{Mod}_{\mathcal{INS}}(\sigma): \mathbf{Mod}_{\mathcal{INS}}(\Sigma')\rightarrow \mathbf{Mod}_{\mathcal{INS}}(\Sigma)$ for each signature morphism $\sigma: \Sigma \rightarrow \Sigma'$.

* For every signature $\Sigma$, a satisfaction relation $\models_{\mathcal{INS}, \Sigma}$ determining the satisfaction of $\Sigma$-sentences by $\Sigma$-models.

* An institution must uphold the satisfaction condition:
for any signature morphism $\sigma:\Sigma \rightarrow \Sigma'$, $\phi \in \textbf{Sen}_{\mathcal{INS}}(\Sigma)$ and $M' \in \lvert\textbf{Mod}_{\mathcal{INS}}(\Sigma')\rvert$, the translations
$\textbf{Mod}_{\mathcal{INS}}(\sigma)$ of models and $\textbf{Sen}_{\mathcal{INS}}(\sigma)$ of
sentences preserve the following satisfaction condition

\begin{equation*}
\label{eq:inssatcond}
M' \models _{\mathcal{INS}, \Sigma'} \textbf{Sen}_{\mathcal{INS}}(\sigma)(\phi)  \quad\iff\quad \textbf{Mod}_{\mathcal{INS}}(\sigma)(M') \models _{\mathcal{INS}, \Sigma} \phi
\end{equation*}

where $\mathbf{Sen}_{\mathcal{INS}}(\sigma)(\phi)$ (resp. $\mathbf{Mod}_{\mathcal{INS}}(\sigma)(M')$) indicates the translation of $\phi$ (resp. reduction of $M'$)  along the signature morphism $\sigma$.

Note that we often denote $\mathbf{Mod}_{\mathcal{INS}}(\sigma): \mathbf{Mod}_{\mathcal{INS}}(\Sigma') \rightarrow \mathbf{Mod}_{\mathcal{INS}}(\Sigma)$ by $\_\rvert_{\sigma}: \mathbf{Mod}_{\mathcal{INS}}(\Sigma') \rightarrow \mathbf{Mod}_{\mathcal{INS}}(\Sigma)$ to indicate the model reduct along a signature morphism $\sigma: \Sigma \rightarrow \Sigma'$. Model reducts are central to the definition of an institution as they allow us to consider a model over one signature as a model over another via a signature morphism.

Institutions have been defined for many different types of logic <cit.>.  One example is the institution of first-order predicate logic with equality, :

The institution for first-order predicate logic with equality, , is composed of the following <cit.> [18, 16]:

Signatures Tuples of the form, $\Sigma_{{\iFOPEQ}} = \langle S, \Omega , \Pi \rangle$, where $S$ is a set of sort names, $\Omega$ is a set of operation names indexed by arity and sort, and $\Pi$ is a set of predicate names indexed by arity. Signature morphisms are sort/arity-preserving functions that rename sorts, operations and predicates.

Sentences For any $\Sigma_{{\iFOPEQ}} = \langle S, \Omega, \Pi \rangle$, $\Sigma_{{\iFOPEQ}}$-sentences are closed first-order formulae built out of atomic formulae using $\wedge, \vee, \lnot, \Rightarrow, {\iff}, \exists, \forall$. Atomic formulae are equalities between $\langle S, \Omega \rangle$-terms, predicate formulae of the form $p(t_1,\ldots, t_n)$ where $p \in \Pi$ and $t_1, \ldots, t_n$ are terms (with variables), and the logical constants  and .

Models Given a signature $\Sigma_{\iFOPEQ} = \langle S, \Omega, \Pi \rangle$,
a model over  consists of a carrier set $\lvert A\rvert _s$ for each sort
name $s \in S$, a function $f_A: \lvert A \rvert _{s_1} \times \dotsb \times
\lvert A\rvert _{s_n} \rightarrow \lvert A\rvert _s$ for each operation name $f \in
\Omega_{s_1 \dotsc s_n,s}$ and a relation $p_A \subseteq \lvert A\rvert _{s_1}
\times \dotsb \times \lvert A \rvert _{s_n}$ for each predicate name $p \in
\Pi_{s_1\dotsb s_n}$, where $s_1,\dotsc,s_n$, and $s$ are sort names.

Satisfaction Relation The satisfaction relation in  is the usual satisfaction of
first-order sentences by first-order structures. This amounts to evaluating the truth of the -formula using the values in the carrier sets and the interpretation of operation and predicate names supplied by the models.

We will use  in Section <ref> as part of the
definition of our Event-B institution.

§.§ Writing Specifications over an Institution

Formally, a specification document written in a specification language is a set of sentences from that language, known as a presentation, which is the basic unit of specification over an institution.

For any signature $\Sigma$, a $\Sigma$-presentation (sometimes called a flat specification) is a pair $\langle \Sigma, \Phi \rangle$ where $\Phi \subseteq \textbf{Sen}(\Sigma)$. $M \in \lvert \textbf{Mod}(\Sigma)\rvert$ is a model of a $\Sigma$-presentation $\langle \Sigma, \Phi \rangle$  if $M \models \Phi$  <cit.>.

Operation     Format     Description
Translation     $SP_1$ with $\sigma$     Renames the signature components of $SP_1$ (sort, operation and predicate names in ) using the signature morphism $\sigma: \Sigma_{SP_1} \rightarrow \Sigma'$. The resulting specification is the same as the original with the appropriate renamings carried out when $\sigma$ is bijective. In the case where $\sigma$ is not surjective then translation adds new symbols. If $\sigma$ is not injective then the signature morphism requires that the interpretations of the symbols identified by $\sigma$ coincide.

Enrichment   $SP_1$ then …    Extends the specification $SP_1$ by adding new sentences after the then specification-building operator. This operator can be used to represent superposition refinement of Event-B specifications by adding new variables and events.

Sum   $SP_1$ and $SP_2$     Combines the specifications $SP_1$ and $SP_2$. It is the most straightforward way of combining specifications with different signatures. This is achieved by forming a specification with a signature corresponding to the union of the signatures of $SP_1$ and $SP_2$. Translation should be used before sum to avoid any unintended name clashes.

Hiding   $SP_1$ hide via $\sigma$     Hiding via the signature morphism $\sigma$ allows viewing a specification, $SP_1$, as a specification containing only the signature components of another specified by the signature morphism $\sigma: \Sigma \rightarrow \Sigma_{SP_1}$. This is useful for representing refinement as it allows a concrete specification to be viewed as one written using only those signature items supported by its corresponding abstract specification.

The basic institution-theoretic specification-building
operators that can be used to modularise specifications in a
formalism-independent manner. Here $SP_1$ and $SP_2$ denote
specifications written over some institution, and $\sigma$ is a
signature morphism in the same institution.

To support modularisation, structured specifications are then built up from flat specifications using the specification-building operators that are available in the theory of institutions <cit.>. These generic specification-building operators are summarised briefly in Table <ref>, and we will demonstrate their use in Event-B in Section <ref>. Note that the intended semantics of a
specification $SP$ is given by its signature, denoted $Sig[SP]$, and its
class of models, $Mod[SP] \subseteq Mod(Sig[SP])$.

§.§ Heterogeneous specification: connecting institutions

Just as we can combine flat and structured specifications within an institution using the specification-building operators, we can combine specifications from different specification languages by defining a mapping between their institutions. This supports the software engineering notion of separation of concerns, allowing us to model different aspects of a specification using different formalisms, each of which is more suited to specifying particular aspects of the system.
An institution comorphism allows the embedding a primitive institution into a more complex one, and we will use it in Section <ref> to define a relationship between  and .

An institution comorphism $\rho:
\mathbf{INS}\rightarrow\mathbf{INS'}$  has three components:

* A functor $\rho^{Sign}: \mathbf{Sign} \rightarrow
\mathbf{Sign'}$.

* A natural transformation $\rho ^{Sen}:
\mathbf{Sen}\rightarrow \rho ^{Sign}; \mathbf{Sen'}$, that is,
for each $\Sigma \in \lvert\mathbf{Sign}\rvert$, a function

$\rho^{Sen}_{\Sigma}: \mathbf{Sen}(\Sigma) \rightarrow
\mathbf{Sen'}(\rho^{Sign}(\Sigma))$.

* A natural transformation $\rho^{Mod}:(\rho^{Sign})^{op};\mathbf{Mod'}\rightarrow \mathbf{Mod} $, that is, for each $\Sigma \in \lvert\mathbf{Sign}\rvert$, a functor
$\rho^{Mod}_{\Sigma}:\mathbf{Mod'}(\rho^{Sign}(\Sigma))\rightarrow \mathbf{Mod}(\Sigma)$.

Further, an institution comorphism must ensure that for any signature $\Sigma
\in \lvert\mathbf{Sign}\rvert$, the translations $\rho^{Sen}_{\Sigma}$
of sentences and $\rho^{Mod}_{\Sigma}$ of models preserve the
satisfaction relation, that is, for any $\psi \in
\mathbf{Sen}(\Sigma)$ and $M' \in
\lvert\mathbf{Mod}(\rho^{Sign}(\Sigma))\rvert$ we have

\rho^{Mod}_{\Sigma}(M') \models_{\Sigma} \psi
\quad\iff\quad
M' \models '_{\rho^{Sign}(\Sigma)}\rho^{Sen}_{\Sigma}(\psi)

and the following diagrams in $\mathbf{Sen}$ and $\mathbf{Mod}$ commute
for each signature morphism in $\mathbf{Sign}$ <cit.>:

Σ_1 [d, "σ"]

𝐒𝐞𝐧(Σ_1) [r, "ρ^Sen_Σ_1 "] [d, "𝐒𝐞𝐧(σ)"']
𝐒𝐞𝐧'(ρ^Sign(Σ_1)) [d, "𝐒𝐞𝐧'(ρ^Sign(σ))" ]

𝐒𝐞𝐧(Σ_2) [r, "ρ^Sen_Σ_2 "']

𝐌𝐨𝐝'(ρ^Sign(Σ_2)) [r, "ρ^Mod_Σ_2 "] [d, "𝐌𝐨𝐝'(ρ^Sign(σ))"']
𝐌𝐨𝐝(Σ_2) [d, "𝐌𝐨𝐝(σ)" ]

𝐌𝐨𝐝'(ρ^Sign(Σ_2)) [r, "ρ^Mod_Σ_1 "']

In summary, this section has outlined the basic definitions that will
be needed to understand our construction of the Event-B institution
that will be presented in Section <ref>.

§ AN OVERVIEW OF THE EVENT-B SPECIFICATION LANGUAGE

In this section, we describe the prerequisite background material that is pertinent to this paper. In particular, Section <ref> briefly outlines the Event-B formal specification language and  Section <ref> introduces a simple example that we will refer to throughout this document. Finally, Section <ref> discusses existing approaches to defining a semantics for Event-B.

§.§ The Syntax for Event-B

The Event-B syntax, consisting of the definition of machines,
contexts and events.  This syntax is does not define the
non-terminals Predicate and Expression, since these
will be mapped to -formulae and terms respectively in our

The abstract syntax for Event-B is described briefly in [2] and we provide a more detailed version in Figure <ref>.   An Event-B specification consists of a set of machine and context definitions.

* Machines encapsulate the dynamic behaviour of a system in terms of a state space, represented by a set of variables and constrained by the machine-level invariants.  A machine contains a set of events, which can be parameterised by values, and are further constrained by the  predicates in the guards, witnesses and actions.  Events are also equipped with a status which is either ,  or  and this is used for proving termination properties with respect to a variant expression defined in the machine.

* Contexts model the static behaviour of a system using sets and constants which can be constrained by axioms.

Both machines and contexts allow the user to specify theorems which are used to generate a specific set of proof obligations. Since these must be consequences of the specification and do not add any additional constraints, we omit them from further discussion here.

In Figure <ref> we do not give a definition for the non-terminals predicate and expression, which we intend to be understood as representing the corresponding concepts from first-order logic.  We will ultimately delegate the semantics of these constructs in Section <ref> to , the institution for first-order predicate logic with equality.
Thus we immediately distinguish two basic sub-languages in Event-B: the
Event-B mathematical language, consisting of predicate logic, set
theory and arithmetic, and the Event-B modelling language which uses these in the definition of events, machines and contexts.

In the spirit of the institutional approach, we can further decompose the Event-B modelling language into two sub-languages which (inspired by an early
version of the UML specification
[49, 50]) we call the
infrastructure language and the superstructure
language. The infrastructure language covers those concepts which are internal to a given context or machine, while the superstructure
language includes the specification-building operators in Event-B.
These constructs allow one machine to refine another, or to see a context, and allow a context to extend other contexts.
It is our thesis that these Event-B operators can be represented and substantially extended using the generic specification-building operators that are part of the institutional framework, and we show how this can be achieved in Section <ref>.

In summary, we divide the constructs of the Event-B language
into three layers, each layer corresponding to one of its three
constituent sub-languages, as illustrated in Figure <ref>.
The right hand side of Figure <ref> shows the
institutional constructs that we will use to define the semantics of each of these constituent sub-languages. This three-layer model plays a key role in structuring the definitions of the functions given in Section <ref>.

text width=0.3*]
[column sep=2mm, row sep=9mm]
[block, align = center] (super) [] Modelling Superstructure;
[block, align = center] (supc) [draw, shape=rectangle] refines, sees;
[block, align = center] (supsbo) []  specification-building operators;

[block, align = center] (ebinf) [] Modelling Infrastructure;
[block, align = center](ebinfc) [draw, shape=rectangle] variables, invariants,
variants, events;
[block, align = center](evtsen) [] -sentences;

[block, align = center](fopeq) [] Mathematical Language;
[block, align = center](fopeqc) [draw, shape=rectangle] carrier sets, constants,
axioms, extends;
[block, align = center] (fopeqsbo) [] -sentences and specification-building operators;

[->, thick] (ebinfc) – (supc);
[->, thick] (fopeqc) – (ebinfc);

We split the Event-B syntax, defined in Figure <ref>, into three sub-languages: superstructure, infrastructure
and a mathematical language.  This figure shows the corresponding
Event-B constructs, and their representation in our semantics.

§.§ A running example illustrating Event-B specification and refinement

We illustrate the use of Event-B via a running example of cars on a bridge that was originally presented in Abrial's book on modelling in Event-B <cit.>. Figure <ref> contains an Event-B specification corresponding to the first abstract machine in this development. It describes the behaviour of cars entering and leaving the mainland. This abstract model is comprised of a context (lines 1–7) specifying a natural number constant $d$ representing the total number of cars, and a basic machine description (lines 8–29) which has a counter $n$ for the number of cars on the island or on the bridge, along with events to initialise the number of cars, and to increase or decrease the counter as cars leave or enter. In this example, the bridge is only wide enough for one car so it can only be used by cars travelling in one direction at any given time.

inv2n ≤d

act1n := 0
act1n := n+1
act1n := n-1

An Event-B specification of an abstract machine
and context . This machine specification consists of the events
and  that model the behaviour of
cars leaving and entering the mainland respectively.

a, b, c
inv1a∈ℕ//on bridge to island
inv2b∈ℕ//on island
inv3c∈ℕ//on bridge to mainland
inv4n = a+b+c
inv5a=0 c=0
thm1a+b+c ∈ℕ theorem
thm2c>0 a>0
$\lor (a+b < d \land c=0)$
$\lor (0<b \land a=0)$ theorem
2*a + b
act2a := 0
act3b := 0
act4c := 0
act1a := a+1
act1a := a-1
act2b := b+1
act1b := b-1
act2c := c+1
act2c := c-1

An Event-B specification of a machine  with
additional events  and  to model the
behaviour of cars entering and leaving the island. The variables
, , and  keep track of the number of
cars on the bridge going to the island, the number of cars on the
island and the number of cars on the bridge going to the mainland

Event-B supports the process of refinement allowing the system specification to be gradually constructed from an abstract specification into a concrete specification [4].
The first refinement step is represented by giving a specification of a concrete machine , shown in Figure <ref>, which is declared to refine  (line 2).  New variables are added to record the number of cars on the bridge going to the island, the number of cars on the island and the number of cars on the bridge going to the mainland (,  and  respectively on line 5) and the invariants on lines 7-15 ensure that these function as expected.

The abstact machine, , is refined by  in two ways.  First, new events are added to describe cars entering and leaving the island ( and  on lines 30–42). Both of these events are defined to be , meaning that they must decrease the value of variant expression defined on line 16.  Second, the events  and  from  are refined to utilise the new variables, ,  and ; their relationship with the abstract events from  is noted explicitly on lines 24 and 44.

§.§ Existing approaches to Event-B semantics

As noted earlier, the only semantic definitions that exist for Event-B have been given in terms of proof obligations which, due to their abstract nature, can inhibit the formal definition of modularisation constructs and interoperability. We discuss these approaches below.

Proof support for Event-B is provided by its Eclipse-based IDE, the  Platform [3]. For each of the specification components listed in Figure <ref>, the  Platform  generates a series of proof obligations which can then be proved automatically and/or interactively using its proving interface.
supports refinement by reusing proofs carried out in an abstract model to prove properties about the concrete model.

This notion of associating a specification with the set of proof obligations it generates can be seen as a form of semantics for those specifications, and this is the approach taken by Hallerstede in his semantics for Event-B [28].  Note that this is not a property-oriented specification, since proof obligations should be theorems of the underlying mathematical context, not axioms that could be used to specify a set of models or define a theory.  By not associating Event-B with any behavioural model, this approach has the advantage of making an Event-B specification independent of any model of computation.  Hallerstede asserts that this facilitates interoperability, since there is no predetermined semantic model to complicate the mapping.

However, this approach also has some disadvantages.  For larger specifications it offers no explicit name-management, and has no formal concept of modularisation.  For example, the semantics of an Event-B machine at the end of a long refinement chain would be a large series of proof obligations collected along the way from different machines and contexts, and with no explicit mention of named events.
In a previous empirical study of a large corpus of Event-B specifications we have found a tendency for monolithic development, with repeated sub-specifications analogous to software code clones [19].
We hypothesise that a more fully developed set of specification-building operators would facilitate the construction of large Event-B specifications in a more modular manner.

Abrial presented a model of Event-B machines in terms of states (variable-to-value mappings) and traces <cit.>.  While Abrial intends these as a justification for the proof obligations, we have used a version of these models in our construction of the Event-B institution in Section <ref>, and we thus define the semantics in this context.
Since the resulting proof obligations will then be part of the theory associated with the model, we anticipate that our approach will be complementary to that of Hallerstede.

There have been other approaches to defining a semantics for elements of the Event-B language, principally in the context of mapping it to other formalisms.  It has been shown that a shallow embedding of the Event-B logic in Isabelle/HOL  provides a sound semantics for the mathematical language of Event-B but not for the full modelling language [57]. Moreover, Event-B is a special form of Back's Action systems which has been formally defined using Dijkstra's weakest precondition predicate transformers [6]. This accounts for the refinement calculus used but not for a full semantic definition of the Event-B modelling language itself.

Other related work includes a CSP semantics for Event-B refinement [60]. This behavioural semantics defines the relationship between the first and last machines in a refinement chain but does not give a semantics for the internal components of these machines.
In previous work, we presented an institution-theoretic approach to  interoperability between Event-B (using the  institution) and CSP (using the  institution) [17]. This work supported heterogeneous specification by constraining the models of -specifications by the models of  ones.

The approach presented in this paper treats Event-B as a complete language rather than as a calculus whose semantics can be given in terms of proof obligations.  Our semantics commits to the theory of institutions, and gets in return a standard set of specification-building operators, along with a generic  framework for interoperability with other formalisms, albeit at the price of including them in the institutional framework.

§ ${\IEVT}$: THE INSTITUTION FOR EVENT-B

This section introduces the  institution, which will play the role of the semantic domains for our semantics: that is, our semantics will map Event-B specifications into structured specifications in the  institution.  The definitions in this section then ensure that these structured specifications have a meaningful semantics.

To define the  institution, Sections <ref> through <ref> give definitions for its basic elements corresponding to Definition <ref>, namely
$\mathbf{Sign_{{\iEVT}}}$, $\mathbf{Sen_{{\iEVT}}}$, $\mathbf{Mod_{{\iEVT}}}$ and the satisfaction relation, $\models_{{\iEVT}}$.  We then prove that the institution-theoretic satisfaction condition holds for .

By default, a structured specification in  represents an Event-B machine.
We handle the Event-B contexts using the institution for first-order predicate logic with equality ( in Definition <ref>), and in Section <ref> we define an institution comorphism from  to  to enable this.   Finally, in Section <ref> we show that  exhibits good behaviour with respect to modularisation by proving properties relating to pushouts and amalgamation in .  This allows us to use the generic specification-building operators of institutions in , and we discuss the pragmatics of this in Section <ref>.

This work was originally presented in [18] and it forms the basis of our definition of a translational semantics in the subsequent sections.

§.§ $\mathbf{Sign}_{\iEVT}$, the Category of $\iEVT$-signatures

Signatures describe the vocabulary that specifications written in a particular institution can have. Here, we define what it means to be an -signature (Definition <ref>) and an -signature morphism (Definition <ref>). We show that $\mathbf{Sign}_{{\iEVT}}$ is indeed a category (Lemma <ref>) which is a necessary requirement for the definition of the  institution.

A signature in  is a five-tuple of sets
$\Sigma_{{\iEVT}} = \langle S, \Omega, \Pi , E, V \rangle$ where

* The first three components form a standard -signature, $\langle S, \Omega, \Pi \rangle$.

* $E$ is a function from event names to their status. We write elements of
this function as tuples of the form $(e\mapsto s)$, for an event named $e$
with a status $s$ which always belongs to the
poset $\{\texttt{ordinary} < \texttt{anticipated} < \texttt{convergent}\}$.

* $V$ is a set of sort-indexed variables.  We write elements of
this set as tuples of the form $(v:s)$, for a variable named $v$
with sort $s \in S$.

In theory it is possible for two variables of different sorts to
share the same name, but we advise against this as it may lead to
confusing specifications.  We assume that $V$ does not
contain any primed variable names and that such names are not
introduced via any signature morphisms.

Following the convention for Event-B [2], we
assume that every signature has an initial event, called
, whose status is always .

We write $\Sigma$ in place of $\Sigma_{{\iEVT}}$ when describing a
signature over our institution for Event-B. For signatures
over institutions other than  we will use the subscript
notation where necessary; e.g. a signature over  is denoted by
$\Sigma_{{\iFOPEQ}}$.  For a given signature $\Sigma$, we access its
individual components using a dot-notation, e.g. $\Sigma.S$ for the
set $S$ in the tuple $\Sigma$.
For any signature, $\Sigma.E$ is a function from event names to their
status, and we will access the domain of this function, $dom(\Sigma.E)$ when
we wish to deal with event names only.

A signature morphism $\sigma: \Sigma \rightarrow \Sigma'$ is a five-tuple containing $\sigma_S$, $\sigma_\Omega$, $\sigma_\Pi$, $\sigma_E$ and $\sigma_V$.  Here $\sigma_S$, $\sigma_\Omega$, $\sigma_\Pi$ are the mappings taken from the corresponding signature morphism in , as follows

* $\sigma_S: \Sigma.S \rightarrow \Sigma'.S$ is a function mapping sort names to sort names.

* $\sigma_\Omega: \Sigma.\Omega \rightarrow \Sigma'.\Omega$ is a family of functions mapping operation names in $\Sigma.\Omega$, respecting the arities and result sorts.

* $\sigma_\Pi: \Sigma.\Pi \rightarrow \Sigma'.\Pi$ is a family of functions mapping the predicate names in $\Sigma.\Pi$, respecting the arities.

* $\sigma_E: \Sigma.E \rightarrow \Sigma'.E$ is a function on
event names and their status with the condition that
for the initial event $\sigma_E ( \texttt{Init}\mapsto
\texttt{ordinary} ) =  (\texttt{Init}\mapsto \texttt{ordinary} )$, while
for non-initial events $\sigma_E$ preserves the status ordering given by the poset
$\{\mathtt{ordinary} < \mathtt{anticipated} <
\mathtt{convergent}\}$.

* $\sigma_V: \Sigma.V \rightarrow \Sigma'.V$ is a function on
sets of variable names whose sorts change according to $\sigma_S$.

Thus if some variable $v$ is renamed to $w$, we must have that
$\sigma(v:s) = (w: \sigma_S(s))$,
where  $\sigma_S$ is the sort mapping as described above.

-signatures and signature morphisms define a category $\mathbf{Sign}_{\iEVT}$. The objects are signatures and the arrows are signature morphisms. Composition of arrows is performed componentwise.

See Appendix.

In this section, we have defined the category of -signatures, $\mathbf{Sign}_{{\iEVT}}$. Next, we define the functor $\mathbf{Sen}_{{\iEVT}}$ that yields -sentences.

§.§ The Functor $\mathbf{Sen}_{\iEVT}$, yielding ${\iEVT}$-sentences

The second component of an institution is a functor called $\mathbf{Sen}$ that generates a set of sentences over a particular signature (Definition <ref>).
Here, we define what is meant by a $\Sigma_{\iEVT}$-Sentence (Definition <ref>) and we prove that $\mathbf{Sen}_{\iEVT}$ is indeed a functor (Lemma <ref>).

Sentences over  are of the form $\langle e, \phi(\overline{x}, \overline{x}\prime) \rangle$. Here, $e$ is an event name in the domain of $\Sigma.E$ (recall that elements of $\Sigma.E$ are functions containing tuples of the form $(e \mapsto \texttt{status})$) and $\phi(\overline{x}, \overline{x}\prime)$ is an open -formula over these variables $\overline{x}$ from $\Sigma.V$ and the primed versions, $\overline{x}\prime$, of the variables.

In the  Platform, Event-B machines are presented (syntactically sugared) as can be seen in abstract form on the left of Figure <ref>. The set of variables in a machine is denoted by $\overline{x}$ (line 2) and the invariants are denoted by $I(\overline{x})$ on line 3. The -signature derived from this machine would look like:
$$\Sigma = \langle S, \Omega, \Pi, \{(
\mathtt{Init}\mapsto \mathtt{ordinary}),  \ldots, (\mathtt{e}_i \mapsto \mathtt{convergent}), \ldots\}, \{\overline{x}\}\rangle$$
where the -component of the signature, $\langle S, \Omega, \Pi \rangle$, is drawn from the “seen” context(s) on line 1.

m a ctx

then act-nameBA(x')
any $\overline{p}$
when guard-nameG(x,p)
with witness-nameW(x,p)
then act-nameBA(x,p,x')

$\{\langle\text{$e$}, I(\overline{x}) \land I(\overline{x}\prime)\rangle \mid e \in dom(\Sigma.E)\}$

$\langle\texttt{Init}, BA(\overline{x}\sp{\prime})\rangle$

$\langle\text{e}_i, n(\overline{x}\prime) < n(\overline{x})\rangle$

$\langle\text{e}, \exists\overline{p} \cdot G(\overline{x},\overline{p}) \land W(\overline{x},\overline{p}) \land BA(\overline{x},\overline{p},\overline{x}\sp{\prime})\rangle$

The elements of an Event-B machine specification as presented
in  (left) and the corresponding sentences in the
institution (right).  The -signature is not shown here, but would
have to be constructed before the sentences.

The variant expression, denoted by $n(\overline{x})$ on line 4, is used for proving termination properties. As described in Section <ref>, events that have a status of  or  must not increase or must strictly decrease the variant expression respectively [2]. Each machine has an  event (lines 6–7) whose action is interpreted as a predicate $BA(\overline{x})$. Events can have parameter(s) as given by the list of identifiers $\overline{p}$ on line 10. $G(\overline{x}, \overline{p})$ and  $W(\overline{x},\overline{p})$ are predicates that
represent the guard(s) and witness(es) respectively over the variables and parameter(s) (lines 11–12). Actions are interpreted as before-after predicates i.e.  is interpreted as . Thus, the predicate $BA(\overline{x},\overline{p},\overline{x}\sp{\prime})$ on line 13 represents the action(s) over the parameter(s) $\overline{p}$ and the sets of variables $\overline{x}$ and $\overline{x}\sp{\prime}$.

Formulae written in the mathematical language (such as the axioms that may appear in contexts) are interpreted as sentences over .  We can include these in specifications over  using the comorphism defined in Section <ref>. We represent the Event-B invariant, variant and event predicates as sentences over . These are illustrated alongside the Event-B predicates that they correspond to in Figure <ref>.

Invariants For each Event-B invariant, $I(\overline{x})$, we form the
open -sentence $I(\overline{x}) \land
I(\overline{x}\prime)$ and pair it with each event name in $\Sigma.$ since invariants apply to all events in a machine.

Thus, we form the set of  event sentences $\{\langle e, I(\overline{x}) \land I(\overline{x}\prime)\rangle \mid e \in dom(\Sigma.E)\}$.

Variants Firstly, we assume the existence of a suitable type for variant expressions and the usual interpretation of the predicates $<$ and $\leq$ over the integers in the signature. In particular, we assume that all specifications include a standard built-in library that defines mathematical operators, such as $<$ and $\leq$, which are axiomatised consistently with their Event-B counterparts. The variant expression applies to specific events, so we pair it with
an event name in order to meaningfully evaluate it. This
expression can be translated into an open -term, which we
denote by $n(\overline{x})$, and we use this to construct a formula
based on the status of the event(s) in the signature $\Sigma$.

* For each $( e \mapsto\texttt{anticipated}) \in \Sigma.E$
we form the -sentence $\langle e, n(\overline{x}\prime) \leq n(\overline{x})\rangle$

* For each $( e \mapsto \texttt{convergent}) \in \Sigma.E$
we form the -sentence $\langle e, n(\overline{x}\prime) < n(\overline{x}) \rangle$

Events Event guard(s) and witnesses are also labelled predicates that can be
translated into open -formulae over the variables
$\overline{x}$ in $V$ and parameters $\overline{p}$. These are denoted
by $G(\overline{x},\overline{p})$ and $W(\overline{x},\overline{p})$
respectively.  In Event-B, actions are interpreted as before-after
predicates, thus they can be translated into open
-formulae denoted by $BA(\overline{x},\overline{p},
\overline{x}\prime)$. Thus for each event we build the formula

$$ \phi(\overline{x}, \overline{x}\prime) \quad=\quad \exists
\overline{p} \cdot G(\overline{x},\overline{p}) \land
W(\overline{x},\overline{p}) \land BA (\overline{x}, \overline{p},
\overline{x}\prime)$$
where $\overline{p}$ are the event parameters. This
is used to build an -sentence of the form $\langle e,
\phi(\overline{x}, \overline{x}\prime)\rangle$.

event, which is an Event-B sentence over only the after
variables denoted by $\overline{x}\prime$, is a special case. In this case, we form the -sentence $\langle \texttt{Init}, \phi(\overline{x}\prime)\rangle$ where $\phi(\overline{x}\prime)$ is a predicate over the after values of the variables as assigned by the  event.

As a further example, Figure <ref> contains the -sentences corresponding to the abstract Event-B specification on lines 1–29 of Figure <ref> excluding those invariants which are used for typing purposes.

$\{\langle$ $e$, d > 0 $\rangle\mid e \in \{\text{Init, ML\_out, ML\_in}\}\}$

$\{\langle$ $e$, n $\leq$ d $\land$ n$\prime$ $\leq$ d $\rangle\mid e \in \{\text{Init, ML\_out, ML\_in}\}\}$

$\langle$ Init, n$\prime$ = 0 $\rangle$
$\langle$ ML_out, n < d $\land$ n$\prime$ = n + 1 $\rangle$
$\langle$ ML_in, n > 0 $\land$ n$\prime$ = n - 1 $\rangle$

These are the -sentences corresponding to the abstract Event-B specification as illustrated on lines 1–29 of Figure <ref>. Note that here the constant, $d$, is interpreted as a 0-ary operator.

There is a functor $\mathbf{Sen}_{\iEVT}: \mathbf{Sign}_{\iEVT} \rightarrow \mathbf{Set}$ generating for each -signature $\Sigma$ a set of -sentences which is an object in the category Set and for each -signature morphism $\sigma: \Sigma_1 \rightarrow \Sigma_2$ (morphisms in the category $\mathbf{Sign}_{\iEVT}$) a function $Sen(\sigma): Sen(\Sigma_1) \rightarrow Sen(\Sigma_2)$ (morphisms in the category Set) translating -sentences.

See Appendix.

In this section, we have defined what is meant by an -sentence. Next, we define -models and the $\mathbf{Mod}_{{\iEVT}}$ functor.

§.§ The Functor $\mathbf{Mod}_{\iEVT}$, yielding ${\iEVT}$-models

construction of -models is based on Event-B mathematical models
as described by Abrial <cit.>.  In these models
the state is represented as a sequence of variable-values and models
are defined over before and after states.
We interpret these states as sets of variable-to-value mappings in our definition
of -models and so we define a $\Sigma$-state of an algebra $A$ in Definition <ref>.

For any given -signature $\Sigma$ we define a
$\Sigma$-state of an algebra $A$ as a set of (sort appropriate) variable-to-value mappings whose domain is the set of sort-indexed variable names
$\Sigma.V$. Note that $A$ is a model for the underlying  signature associated with $\Sigma$.
We define the set $State_{A}$ as the set of all such  $\Sigma$-states. By
“sort appropriate” we mean that for any variable $x$ of sort $s$ in
$V$, the corresponding value for $x$ should be drawn from $\lvert A\rvert _s$, the
carrier set of $s$ given by a -model $A$.

Essentially, a $\Sigma$-state$_A$ corresponds to valuations in the
$\Sigma_{\iFOPEQ}$-model, $A$, of the variables in $\Sigma.V$.

Given $ \Sigma = \langle S, \Omega, \Pi, E, V \rangle$,
$\mathbf{Mod}_{\iEVT}(\Sigma)$ provides a category of -models, where an
-model over $\Sigma$ is a tuple $\langle A, L, R \rangle$ where

* $A$ is a $\Sigma_{{\iFOPEQ}}$-model.

* $L \subseteq State_{A}$ is the non-empty initialising set that provides the
states after the  event. We note that trivial models are excluded as the initialising set $L$ is never empty. We can see this because even in the extreme cases where there are no predicates or variables in the $\mathtt{Init}$ event, $L$ is the singleton containing the empty map $(L=\{\{\}\}$).

* For every event name, $e$, in the domain of $E$, denoted by $e\in dom(E)$, other than , we define $R.e \subseteq State_{A} \times State_{A}$ where for each pair of states $\langle s, s\prime\rangle$ in $R.e$, $s$ provides values for the variables $x$ in $V$, and $s\prime$ provides values for their primed versions $x\prime$.
$R = \{R.e \mid e \in dom(E) \ and \ e \neq \texttt{Init}\}$.

Intuitively, a model over $\Sigma$ maps every event name $e$ in $(\Sigma.E)$ to a  set of variable-to-value mappings over the carriers corresponding to the sorts of each of the variables $x \in \Sigma.V$ and their primed versions $x\prime$.
For example, given the event  on the left of Figure <ref>, with natural number
variable  and boolean variable  we
construct the variable-to-value mappings on the right of Figure <ref>.

when grd1x<2
then act1x := x + 1
act2y :=

$$R_e = \left\{\begin{array}{llll}
\{ \maplet{x}{0},& \maplet{y}{false},&
\maplet{x'}{1},& \maplet{y'}{false} \},
\\
\{ \maplet{x}{0},& \maplet{y}{true},&
\maplet{x'}{1},& \maplet{y'}{false} \},
\\
\{ \maplet{x}{1},& \maplet{y}{false},&
\maplet{x'}{2},& \maplet{y'}{false} \},
\\
\{ \maplet{x}{1},& \maplet{y}{true},&
\maplet{x'}{2},& \maplet{y'}{false} \}
\end{array}\right\}$$

The left hand side shows an example of an Event-B event, $e$,
with natural number variable $x$ and boolean variable $y$. When
$x>2$, the event increments the value of $x$ and changes $y$ to
. The right hand side enumerates $R_e$, the corresponding set
of variable-to-value mappings for the event on the left.

The notation used in this example
is interpreted as $\maplet {\textit{variable name}}
{\textit{value}}$ which is a data state where the
value is drawn from the carrier set corresponding to the sort of the
variable name given in $\Sigma.V$.

The proof requirement here is to show that
$\mathbf{Mod}_{{\iEVT}}(\Sigma)$ forms a category for a given
-signature $\Sigma$.
For any -signature $\Sigma$ there is a category of -models $\mathbf{Mod}_{\iEVT}(\Sigma)$ where the objects in the category are -models and the arrows are -model morphisms.

See Appendix.

Model reducts are central to the definition of an institution (Definition <ref>) and in Definition <ref>, we define the -model reduct. Then, in Lemma <ref>, we prove that the -model reduct is a functor.

The reduct of an -model $M=
\langle A, L,
R \rangle$ along an -signature morphism $\sigma: \Sigma
\rightarrow \Sigma'$ is given by $M\rvert _\sigma = \langle A\rvert _\sigma,
L\rvert_\sigma, R\rvert_\sigma\rangle$. Here $A\rvert _\sigma$ is the reduct of the
-component of the -model along the -components of $\sigma$. $L\rvert_\sigma$ and $R\rvert _\sigma$ are based on the reduction of the states of $A$ along $\sigma$, i.e. for every $\Sigma'$-state $s$ of $A$, that is for every sorted map $s : \Sigma'.V \rightarrow \lvert A\rvert$, $s\rvert _{\sigma}$ is the map $\Sigma'.V \rightarrow \lvert A\rvert$ given by the composition $\sigma_{V} ; s$. This extends in the usual manner from states to sets of states and to relations on states.

For each -signature morphism $\sigma: \Sigma_1 \rightarrow \Sigma_2$ the -model reduct is a functor $\textbf{Mod}(\sigma)$ from $\Sigma_2$-models to $\Sigma_1$-models.

See Appendix.

There is a functor $\mathbf{Mod}_{\iEVT}$ yielding a category $\mathbf{Mod}(\Sigma)$ of -models for each -signature $\Sigma$, and for each -signature morphism $\sigma: \Sigma_1 \rightarrow \Sigma_2$ a functor $\mathbf{Mod}(\sigma)$ from $\Sigma_2$-models to $\Sigma_1$-models.

See Appendix.

In this section, we defined -models, model reducts and the $\mathbf{Mod}_{{\iEVT}}$ functor. Next, we describe the satisfaction relation, $\models_{{\iEVT}}$, in  and prove that  is a valid institution.

§.§ The Satisfaction Relation for ${\iEVT}$

All institutions are equipped with a satisfaction relation to evaluate if a particular model satisfies a sentence. Here, we define the satisfaction relation for .
In order to define the satisfaction relation for , we describe
an embedding from -signatures and models to
-signatures and models.

Given an -signature $\Sigma = \langle S, \Omega, \Pi, E, V \rangle$ we form the following two -signatures:

* $\Sigma^{(V,V\prime)}_{{\iFOPEQ}} = \langle S, \Omega\cup V \cup V', \Pi\rangle$  where
$V$ and $V'$ are the variables and their primed versions,
respectively, that are drawn from the -signature, and
represented as $0$-ary operators with unchanged sort.
The intuition
here is that the set of variable-to-value mappings for the free
variables in an -signature $\Sigma$ are represented as expansions of $A$
along the signature inclusion obtained by adding a distinguished $0$-ary operation
symbol to the corresponding -signature for each of the variables $x \in V$ and
their primed versions.

* Similarly, for the initial state and its variables, we construct
the signature $\Sigma^{(V')}_{{\iFOPEQ}}= \langle S,
\Omega\cup V', \Pi\rangle$.

Given the  $\Sigma$-model $\langle A,L,R \rangle$, we construct
the -models:

* For every pair of states $\langle s,s' \rangle$, we form the
$\Sigma^{(V,V')}_{{\iFOPEQ}}$-model expansion $A^{(s, s')}$,
which is the -component $A$ of the -model, with
$s$ and $s'$ added as interpretations for the new operators that
correspond to the variables from $V$ and $V'$ respectively.

* For each initial state $s' \in L$ we construct the
$\Sigma^{(V')}_{{\iFOPEQ}}$-model expansion $A^{(s')}$ analogously.

For any -sentence over $\Sigma$ of the form
$\langle e, \phi(\overline{x}, \overline{x}') \rangle$, we create a
corresponding -formula by replacing the free variables with
their corresponding operator symbols.  We write this (closed) formula
as $\groundevt$.

Given these -signatures and models, we now define the satisfaction relation for  in Definition <ref>.

We define the satisfaction relation in  as follows.  We specify satisfaction for initial events over $L$ and non-initial events over $R$.
For any -model $\langle A,L,R \rangle$ and
-sentence $\langle e, \phi(\overline{x}, \overline{x}\prime)
\rangle$, where $e$ is an event name other than , we define:

\langle A,L,R \rangle \models_{\Sigma}
\langle e, \phi(\overline{x}, \overline{x}') \rangle
\quad \iff \quad
\forall \langle s,s' \rangle \in R.e \cdot A^{(s, s\prime)}
\models_{{\Sigma^{(V,V')}_{\iFOPEQ}}} \groundevt

Similarly, we evaluate the satisfaction relation of -sentences of the form $\langle \texttt{Init}, \phi(\overline{x}')\rangle $ as follows:

$\langle A,L,R \rangle
\models_{\Sigma}
\langle \mathtt{Init}, \phi(\overline{x}') \rangle
\quad \iff \quad
\forall s'  \in L \cdot A^{(s\prime)}  \models_{{\Sigma^{(V')}_{\iFOPEQ}}} \groundevtinit$

Given  signatures $\Sigma_1$ and $\Sigma_2$, a signature morphism
$\sigma: \Sigma_1 \rightarrow \Sigma_2$, a $\Sigma_2$-model $M_2$ and a $\Sigma_1$-sentence $\psi_1$, the following satisfaction condition holds:

$ \mathbf{Mod}(\sigma)(M_2)\models_{{\iEVT}_{\Sigma_1}} \psi_1 \quad \iff \quad M_2 \models_{{\iEVT}_{\Sigma_2}} \mathbf{Sen}(\sigma)(\psi_1)$

We must prove this for -sentences of the form $\langle e, \phi(\overline{x}, \overline{x}')\rangle$ as defined in Definition <ref>, with the satisfaction relation, $\models_{{\iEVT}}$, as defined in Definition <ref>. Let $M_{2}$ be the -model $\langle A_{2}, L_{2}, R_{2} \rangle$, and let $\psi_{1}$ be the -sentence $\langle e, \phi(\overline{x}, \overline{x}') \rangle$, then the satisfaction condition is equivalent to

$ \forall \langle s, s' \rangle \in R_2\rvert _{\sigma}.e \cdot  (A_2\rvert _{\sigma})^{(s, s\prime)}\rvert _\sigma \models_{{\iFOPEQ}_{\Sigma^{(V_1,V_1\prime)}_{\iFOPEQ}}} \groundevt$

$ \iff \forall \langle s, s' \rangle \in R_2.\sigma_{E}(e) \cdot A_2^{(s, s\prime)}  \models_{{\iFOPEQ}_{\Sigma^{(V_2,V_2\prime)}_{\iFOPEQ}}} Sen(\sigma)(\groundevt)$

Here, validity follows from the validity of
satisfaction in . We prove the result for initial
events in the same way.

Since validity follows from that  of , we thus conclude that  preserves the satisfaction condition required of an institution.

In this section we have presented the satisfaction relation in  and showed that  preserves the axiomatic property of an institution (satisfaction condition in Theorem <ref>). As the satisfaction relation in  (Definition <ref>) relied on a  embedding of signatures and models, we discuss the relationship between  and  in Section <ref>.

§.§ Specifying Event-B contexts by relating ${\iFOPEQ}$ and ${\iEVT}$

Initially, we defined the relationship between  and
to be a duplex institution formed from a restricted version of
($_{res}$) and  where $_{res}$ is the
institution  but does not contain any
components. Duplex institutions are constructed by enriching one
institution by the sentences of
another ($_{res}$ is enriched by sentences from ) using an institution semi-morphism
[23] <cit.>. This approach would allow us to
constrain $_{res}$ by  and thus facilitate the use of
-sentences in an elegant way.  However, duplex institutions
are not supported in , the only tool-set currently available for institutions [46],
and therefore we opt for a comorphism (Definition <ref>) which embeds the simpler
institution  into the more complex institution

We define $\rho: {\iFOPEQ} \rightarrow {\iEVT}$ to be an institution comorphism
composed of:

* The functor $\rho^{Sign}: \mathbf{Sign}_{{\iFOPEQ}} \rightarrow
\mathbf{Sign}_{{\iEVT}}$ which takes as input a -signature of the form $\langle S, \Omega, \Pi \rangle$ and extends it with the set  $E=\{(\texttt{Init} \mapsto \texttt{ordinary})\}$ and an empty set of variable names $V$. Here, $\rho^{Sign}(\sigma)$ works as $\sigma$ on $S$, $\Omega$ and $\Pi$, it is the identity on the  event and the empty function on the empty set of variable names.

* The natural transformation  $\rho^{Sen}: \mathbf{Sen}_{{\iFOPEQ}} \rightarrow \rho^{Sign};\mathbf{Sen}_{{\iEVT}}$ which treats any closed -sentence (given by $\phi$) as an Event-B invariant sentence, to form the set of -sentences $\{ \langle e, \phi\rangle \mid e \in dom(\Sigma .E)\}$. As there are no variables in the signature, and $\phi$ is any closed formula, we do not require $\phi$ to be over the variables $\overline{x}$ and $\overline{x}\prime$.

* The natural transformation $\rho^{Mod}: (\rho^{Sign})^{op} ;\mathbf{Mod}_{{\iEVT}} \rightarrow \mathbf{Mod}_{{\iFOPEQ}}$
is such that for any -signature $\Sigma$ and -model $\langle A, L, \emptyset\rangle$ for $\rho^{Sign}(\Sigma)$ then

$\rho^{Mod}_{\Sigma}(\langle A, L, \emptyset\rangle) = A$

Next, we prove that $\rho:{\iFOPEQ}\rightarrow{\iEVT}$ meets the axiomatic requirements of an institution comorphism.

The institution comorphism $\rho$ is defined such that for any $ \Sigma \in \lvert \mathbf{Sign}_{{\iFOPEQ}}\rvert$, the translations $\rho^{Sen}_{\Sigma}: \mathbf{Sen}_{{\iFOPEQ}}(\Sigma) \rightarrow \mathbf{Sen}_{{\iEVT}}(\rho^{Sign}(\Sigma))$ and $\rho^{Mod}_{\Sigma}: \mathbf{Mod}_{{\iEVT}}(\rho^{Sign}(\Sigma)) \rightarrow \mathbf{Mod}_{{\iFOPEQ}}(\Sigma)$ preserve the satisfaction relation.
That is, for any $\psi \in \mathbf{Sen}_{{\iFOPEQ}}(\Sigma)$ and $M' \in \lvert\mathbf{Mod}_{{\iEVT}}(\rho^{Sign}(\Sigma))\rvert$

\begin{equation*}
\rho^{Mod}_{\Sigma}(M') \models_{{\iFOPEQ}_{\Sigma}} \psi \; \iff \; M' \models_{{\iEVT}_{\rho^{Sign}(\Sigma)}} \rho^{Sen}_{\Sigma}(\psi) \label{eqn:comor}\end{equation*}

By Definition <ref>, $M' = \langle A, L, \emptyset \rangle$, $\rho^{Mod}_{\Sigma}(M') = A$ and
$\rho^{Sen}_{\Sigma}(\psi) = \{ \langle e , \psi\rangle \mid e \in dom(\Sigma .E)\}$. Therefore, the above equivalence becomes

$$A \models_{{\iFOPEQ}_{\Sigma}} \psi
\; \iff \;
M' \models_{{\iEVT}_{\rho^{Sign}(\Sigma)}} \{ \langle e, \psi\rangle \mid e \in dom(\Sigma .E)\}

Then, by the definition of the satisfaction relation in  (Definition <ref>) we get the following for each $\psi$ in $\{ \langle e, \psi\rangle \mid e \in dom(\Sigma .E)\}$.

A \models_{{\iFOPEQ}_{\Sigma}} \psi
\; \iff \;
\forall s\prime \in L \cdot A^{( s\prime)} \models_{{\iFOPEQ}_{(\rho^{Sign}(\Sigma))^{(V')}_{{\iFOPEQ}}}} \psi

We deduce that $\Sigma = (\rho^{Sign}(\Sigma))^{V'}_{{\iFOPEQ}}$,
since there are no variable names in $V'$ and thus no new operator symbols are added to the signature. As there are no variable names in $V'$, we have $L=\{\{\}\}$, so we can conclude that $A^{(s\prime)} = A$.

Thus the satisfaction condition holds.

Using the comorphism.
The purpose of this comorphism is to allow us to use  specifications in .
Thus, given the institution comorphism $\rho:{\iFOPEQ} \rightarrow {\iEVT}$,
for any $\Sigma$-specification written over  we can use the
specification-building operator
$$\_\_ \texttt{ \ikw{with} } \rho:
Spec_{{\iFOPEQ}}(\Sigma) \rightarrow

to interpret this as a specification over
<cit.>. This results in
a specification with just the  event and
no variables, containing -sentences that hold in the initial state.
This process is used to represent contexts, specifically
their axioms, which are written over  as sentences over

We note that there is a dual nature to the relationship between  and . The first being the use of  to evaluate the -satisfaction condition via an embedding as presented in Section <ref>. The second is the comorphism that we have described above which allows us to project Event-B context sentences into  and we illustrate this in our  semantics in Section <ref>. This double relationship offers a number of interesting consequences. In a way,  is tied to  in terms of the evaluation of the satisfaction relation. However, the use of the comorphism to represent context sentences means that it is possible to replace this use of  with another logic so long as a comorphism can be defined to . This second relationship illustrates the plug `n' play nature of the  institution.

In cases where a specification is enriched with new events, then the axioms and invariants should also apply to these new events. Our use of -sentences that define invariants mediates this as they are applied to all events in the specification when evaluating the satisfaction condition.
In order for an institution to correctly utilise the specification-building operators, we must prove properties with regard to pushouts and amalgamation. We prove that  meets these requirements in Section <ref>.

§.§ Enabling specification-building via pushouts and amalgamation

We ensure that the  institution has good modularity properties
by proving that  admits the amalgamation property: all pushouts
in Sign$_{{\iEVT}}$ exist and every pushout diagram in
Sign$_{{\iEVT}}$ admits weak model amalgamation
<cit.>. Note that the weak amalgamation property corresponds to the usual definition of amalgamation with the uniqueness constraint dropped <cit.>.

This requirement was actually first referred to as “exactness" and defined by Diaconescu et al. [14]. In [56],
structured specifications are built by consecutive application of these
specification-building operators. The meaning of structured specifications is obtained by applying functions that correspond to the specification-building operators on the associated signatures and model classes. In particular, the signature (resp. model class) corresponding to a structured  specification that uses the and specification-building operator is obtained using the pushout (resp. amalgamation) construction shown below <cit.>.

Pushouts exist in Sign$_{{\iEVT}}$.

See Appendix.

In Definition <ref> we present the definition of amalgamation as outlined by Sannella and Tarlecki and use it to structure the proof of amalgamation in  <cit.>.

Let $\mathbf{INS} = \langle \mathbf{Sign}, \mathbf{Sen}, \mathbf{Mod}, \langle \models_{\Sigma} \rangle_{\Sigma \in \lvert\mathbf{Sign}\rvert}\rangle$ be an institution. The following diagram in $\mathbf{Sign}$

(P0) at (90:2cm) $\Sigma$;
(P1) at (90+90:2.5cm) $\Sigma_1$ ;
(P3) at (90+3.75*72:2.5cm) $\Sigma_2$;
(P2) at (90+2*90:2cm) $\Sigma'$;
[commutative diagrams/.cd, every arrow, every label]
(P0) edge node [swap]$\sigma_1$ (P1)
(P1) edge node  $\sigma_1'$ (P2)
(P3) edge node[swap] $\sigma_2'$ (P2)
(P0) edge node $\sigma_2$ (P3);

admits amalgamation if

* for any two models $M_1 \in \lvert \mathbf{Mod}(\Sigma_1) \rvert$ and $M_2 \in \lvert \mathbf{Mod}(\Sigma_2) \rvert$, there exists a unique model $M' \in \lvert \mathbf{Mod}(\Sigma') \rvert$ (amalgamation of $M_1$ and $M_2$) such that $M'\rvert _{\sigma_1'} = M_1$ and $M'\rvert _{\sigma_2'} = M_2$.

* for any two model morphisms $f_1:M_{11} \rightarrow M_{12}$ in $\mathbf{Mod}(\Sigma_1)$ and $f_2:M_{21} \rightarrow M_{22}$ in $\mathbf{Mod}(\Sigma_2)$ such that $f_1\rvert_{\sigma_1} = f_2\rvert_{\sigma_2}$, there exists a unique model morphism $f':M_1' \rightarrow M_2'$ in $\mathbf{Mod}(\Sigma')$ (amalgamation of $f_1$ and $f_2$) such that $f'\rvert_{\sigma_1'} = f_1$ and $f'\rvert_{\sigma_2'} = f_2$.

The institution $\mathbf{INS}$ has the amalgamation property if all pushouts exist in $\mathbf{Sign}$ and every pushout diagram in $\mathbf{Sign}$ admits amalgamation <cit.>.

Every pushout diagram in Sign$_{{\iEVT}}$ admits weak model amalgamation.

See Appendix

So far, we have defined our institution for Event-B, , outlined the comorphism from  to , and shown that  meets the requirements needed for correct use of the specification-building operators. Next, we discuss the pragmatics of specification-building in  (Section <ref>).

§.§ Some pragmatics of Specification Building in ${\iEVT}$

We represent an Event-B specification, that is composed of machines and contexts, as a structured specification that is built from flat specifications (presentations in Definition <ref>) over  using the specification-building operators. Technically,  allows for loose specifications which are not possible in Event-B, however, we do not exploit this in our examples that follow.

Recall that, for any
signature $\Sigma$, a $\Sigma$-presentation is a set of
$\Sigma$-sentences. A model of a $\Sigma$-presentation is a
$\Sigma$-model that satisfies all of the sentences in the presentation
[23].  Thus, for a presentation in , model
components corresponding to an event must satisfy all of the sentences
specifying that event.  This incorporates the standard semantics of the
extends operator for events in Event-B where the extending
event implicitly contains all the parameters, guards and actions of the
extended event but can include additional parameters, guards and actions

An interesting aspect is that if a variable is not assigned a value, within
an action, then a model for the event may associate a new value with
this variable.  Some languages deal with this using a frame
condition, asserting implicitly that values for unmodified
variables do not change.  In Event-B such a condition would cause
complications when combining presentations, since variables
unreferenced in one event will be constrained not to change, and this
may contradict an action for them in the other event.  As far as we
can tell, the informal semantics for the Event-B language does not
require a frame condition, and we have not included one in our definition.

§ A FORMAL SEMANTICS FOR EVENT-B

In the previous sections, we described the Event-B formal specification language and the  institution which provides the target for our translational semantics. This section is the centrepiece of this paper and shows how we map from the constructs of the Event-B language into the semantic domains given by .
Our objective is to define a formal semantics for Event-B by representing Event-B specifications as structured specifications over , our institution for Event-B [18]. Our approach is structured around the three constituent sub-languages of Event-B that we identified in Section <ref>.

Exploiting the three-layer model:

We utilise our three-layer model of the Event-B language that was presented in Figure <ref> in order to translate Event-B into the institutional framework as follows.

* At the base of Figure <ref> is the Event-B mathematical language. The institution of first-order predicate logic with equality, , is embedded via an institution comorphism (Definition <ref>) into the institution for Event-B,  [18]. The semantics that we define translates the constructs of this mathematical language into corresponding constructs over .

* At the next level is the Event-B infrastructure, which consists of those language elements used to define variables, invariants, variants and events. These are translated into sentences over .

* At the topmost level is the Event-B superstructure which deals with the definition of Event-B machines and contexts, as well as their relationships (, , ). These are translated into structured specifications over  using the specification-building operators.

Closely following the syntax defined in Figure <ref>, we
define the semantics of each of the Event-B language elements by
describing a mechanism to translate them into -sentences. In
order to carry out such a translation we first extract the
corresponding -signature $\Sigma = \langle S, \Omega, \Pi, E, V
\rangle$ from any given Event-B specification. Contexts can be
represented entirely by the underlying mathematical language and thus
translated into specifications over , and embedded using the

In Section <ref>, we define an interface (Figure
<ref>) in order to facilitate the use of some
operations and functions.  We provide functions for
extracting the signature of an Event-B specification in Section
<ref>. In a bottom-up fashion, Sections <ref> and
<ref> define the semantics of the Event-B infrastructure and
superstructure languages respectively.

§.§ The ${\iFOPEQ}$ Interface

Just as the Event-B formalism is built on an underlying mathematical
language, our institution for Event-B is founded on , the
institution for first-order predicate logic with equality. In Figure
<ref>, we define a  interface in order to
facilitate the use of its operations and functions in our
definitions. The description of these operations is outlined in Figure
<ref> and not specified further.

The function $\mathbb{P}_\Sigma$ described in Figure <ref> takes a labelled predicate and outputs a -sentence ($\Sigma$-formula).
The function $\mathbb{T}_\Sigma$ takes an expression and returns a $\Sigma$-term. These functions are used to translate Event-B predicates and expressions into $\Sigma$-formulae and $\Sigma$-terms respectively.

The purpose of the function $\mathbb{M}$ is to take two lists of identifiers and a list of labelled predicates and, use these to form the  signature $\langle S,\Omega,\Pi \rangle$. The reason for this is that when extracting a signature from a context (described in Figure <ref>) carrier sets are interpreted as sorts and used to form $S$. The constants and axioms are used to form $\Omega$ and $\Pi$. We assume that $\mathbb{M}$ provides this translation.

* $\mathtt{F.and} : \Sigma\textit{-formula}^*  \rightarrow \Sigma\textit{-formula}$

This corresponds to the logical conjunction ($\land$) of a set of formulae in .

* $\mathtt{F.lt} : \Sigma\textit{-term} \times \Sigma\textit{-term} \rightarrow \Sigma\textit{-formula}$

This operation takes two terms and returns a formula corresponding to arithmetic less than ($<$).

* $\mathtt{F.leq} : \Sigma\textit{-term}\times \Sigma\textit{-term} \rightarrow \Sigma\textit{-formula}$

This operation takes two terms and returns a formula corresponding to arithmetic less than or equal to ($\leq$).

* $\mathtt{F.exists} : VarName^* \times \Sigma\textit{-formula} \rightarrow \Sigma\textit{-formula}$

This operation takes a sequence of $VarName$s and a formula and returns a formula corresponding to the existential quantification of the $VarName$s over the input formula.

* $\mathtt{F.}\iota : VarName ^* \rightarrow \Sigma\textit{-formula} \rightarrow \Sigma\textit{-formula}$

This operation takes a list of $VarName$s and formula and returns the input formula with the names of all of the free variables (as given by the list of $VarName$s) primed.

* $\mathbb{P}_\Sigma: LabelledPred \rightarrow \Sigma\textit{-formula}$

* $\mathbb{T}_\Sigma: Expression\rightarrow \Sigma\textit{-term}$

* $\mathbb{M}: SetName ^* \times ConstName^*  \times LabelledPred^* \rightarrow \lvert \textbf{Sign}_{{\iFOPEQ}}\rvert$

The  interface provides access to a range of operations and functions which we assume to exist. These are used throughout our definitions in Figures <ref>, <ref> and <ref>.

For simplicity, we assume that it is possible to use Event-B identifiers in  and . Also, when we reference a $\Sigma\textit{-formula}$ in Figure <ref> we mean a possibly open -formula over the signature given by $\Sigma$. We only return a closed -formula when applying $\mathbb{P}_{\Sigma}$ to axiom sentences since they form closed predicates in Figure <ref>.

§.§ Extracting the Signature

For an Event-B specification $SP$, we form an environment $\xi = \mathbb{D}\BR{SP}\xi_0$ where  $\xi_0$ is the empty environment.

\bullet &Env & = (MachineName \cup ContextName) \rightarrow |\mathbf{Sign}|  \quad \Comment{An environment maps names to signatures}\\
\\
\bullet & \mathbb{D}:& Specification \rightarrow Env \rightarrow Env
\Comment{Process a list of machine/context definitions}\\[2pt]
&\mathbb{D} & \BR{\langle ~ \rangle}\; \xi \;=\; \xi\\
&\mathbb{D} & \BR{hd :: tl}\; \xi \;=\; \mathbb{D} \;(\BR{tl}) \;(\mathbb{D} \;\BR{hd} \;\xi)\\
\\
\bullet & \mathbb{D}: & Machine \rightarrow Env \rightarrow Env
\Comment{Extract and store the signature for one machine}\\[2pt]
&\mathbb{D} & \left\llbracket\begin{array}{l}
\texttt{machine } m \\
\texttt{refines }  a \\
\texttt{sees }  ctx_1, \ldots,ctx_n  \\
\texttt{end}\\
\end{array}\right\rrbracket\; \xi
\;=\;
\xi  \cup \{ \llbracket m \rrbracket \mapsto (\langle S, \Omega, \Pi, E, V\rangle \ \ikw{$\cup$} \ r( \xi \BR{a}))\}\\
&&where \\
&&  \qquad \langle S, \Omega, \Pi \rangle \;=\;
\{(\xi\; \BR{ctx_1}) \ \ikw{$\cup$} \ \ldots  \ \ikw{$\cup$} \ (\xi \;\BR{ctx_n})\}
\Comment{Include signatures from `seen' contexts}\\
&& \qquad  \langle E, V, RA \rangle \;=\;
\mathbb{D} \BR{mbody}
\Comment{Collect names from machine body}\\
&&and \\
&& \qquad r \;:\; |\textbf{Sign}_{\iEVT}| \rightarrow |\textbf{Sign}_{\iEVT}| \Comment{Signature for the abstract machine (less the refined events)}\\
&& \qquad r (\xi \BR{a}) \;=\;
\texttt{let } \Sigma_a = \xi \BR{a} \texttt{ in } \langle \Sigma_a.S,\, \Sigma_a.\Omega,\,  \Sigma_a.\Pi,\,  RA \ndres \Sigma_a.E,\, \Sigma_a.V \rangle \\
\\
\bullet & \mathbb{D}: & MachineBody  \rightarrow
(\setof{EventName \times Stat} \times \setof{VarName} \times \setof{EventName} )\\
&&\Comment{Extract signature elements from machine-body} \\[-2ex]
&\mathbb{D} & \left\llbracket\begin{array}{l}
\texttt{variables }  v_1, \ldots , v_n \\
\texttt{invariants }  i_1, \ldots , i_n \\
\texttt{theorems }  t_1, \ldots , t_n \\
\texttt{variant }  n  \\
\texttt{events }  e_{init} \ e_1,\ldots,e_n \\
\end{array}\right\rrbracket
\;=\;
\langle E, V, RA \rangle \\
&&where \\
&& \qquad  E \;=\; \{\emph{def}\,\BR{e_{init}},\emph{def}\,\BR{e_1}, \ldots, \emph{def}\,\BR{e_n}\}
\Comment{Names of events defined here}\\
&& \qquad  V \;=\; \langle \BR{v_1}, \ldots, \BR{v_n} \rangle
\Comment{Names of variables declared here}\\
&& \qquad RA \;=\; \emph{ref}\,\BR{e_{init}} \cup \emph{ref}\,\BR{e_1} \cup \ldots \cup \emph{ref}\,\BR{e_n}
\Comment{Names of (abstract) events refined here}\\
\\
\bullet & \emph{def}: & Event \rightarrow (EventName \times Stat)
\Comment{Extract event name \& status from an event definition}\\[2pt]
&\emph{def} & \BR{\texttt{event }e, \texttt{status } s, \texttt{refines } e_1, \ldots, e_n,  \cdots \texttt{end}} \;=\; (e\mapsto s )\\
&\emph{def} & \BR{e_{init}} \;=\; \langle \mathtt{Init}, \mathtt{ordinary} \rangle\\
\\
\bullet & \emph{ref}: &Event \rightarrow \setof{EventName}
\Comment{Extract names of refined events from an event definition}\\[2pt]
&\emph{ref}& \BR{\texttt{event } e, \texttt{status } s, \texttt{refines } e_1, \ldots, e_n,  \cdots \texttt{end}}
\;=\;
\{\BR{e_1}, \ldots, \BR{e_n}\}\\
&\emph{ref}&\BR{e_{init}} = \{\BR{e_{init}}\}\\
\\

\bullet & \mathbb{D}: & Context \rightarrow Env \rightarrow  Env
\Comment{Extract and store the signature for one context}\\[2pt]
&\mathbb{D} & \left\llbracket\begin{array}{l}
\texttt{context } ctx \\
\texttt{extends } ctx_1,\ldots,ctx_n \\
\texttt{end}
\end{array}\right\rrbracket \xi
\;=\;
\xi \;\cup\; \{\BR{ctx} \mapsto \begin{array}{l}
(\mathbb{D}\BR{cbody} \mathbin{\ikw{$\cup$}} \xi \BR{ctx_1} \mathbin{\ikw{$\cup$}}
\ldots \mathbin{\ikw{$\cup$}} \xi \BR{ctx_n})\}\\
\end{array}
\\
\\
\bullet & \mathbb{D}: & ContextBody \rightarrow  \lvert\textbf{Sign}_{{\iFOPEQ}}\rvert
\Comment{Extract the {\iFOPEQ} signature from a context body}
\\[2pt]
&\mathbb{D} & \left\llbracket\begin{array}{l}
\texttt{sets } s_1,\ldots,s_n \\
\texttt{constants } c_1, \ldots, c_n\\
\texttt{axioms }  a_1, \ldots , a_n \\
\texttt{theorems } t_1, \ldots ,t_n \\
\end{array}\right\rrbracket
\;=\; \langle S, \Omega, \Pi \rangle
\Comment{Sorts, operations, predicates}\\
&& where \\
&& \qquad  \langle S, \Omega, \Pi \rangle  = \mathbb{M}((\BR{s_1},\ldots,\BR{s_n}),\; (\BR{c_1}, \ldots ,\BR{c_n}),\; (\BR{a_1}, \ldots ,\BR{a_m}))\\
\end{array}$
These auxiliary functions are used to extract a signature from an Event-B specification, which is a  list of context or machine definitions.  The extraction of -signatures uses the interface functions described in Figure <ref>.

Before we form sentences in any institution, we must first specify the corresponding signature.
To aid this process, we define $Env$ to be the type of all
environments, which are just mappings from machine/context names to
their corresponding signature. In all subsequent definitions we use
$\xi$ to denote an environment of type $Env$. We define the overloaded function $\mathbb{D}$ in Figure <ref> to build the environment from a given Event-B specification, which is a list of machine and context definitions.

The function $def$ (Figure <ref>) extracts the function $($event name $\mapsto$ status$)$ for each event in the machine and these functions form the $E$ component of the signature. Each event name is tagged with a status in order to correctly form variant sentences which will be discussed in Section <ref>. The function $ref$ (Figure <ref>) forms the set of events that a particular concrete event refines. We use this function to remove the names of the refined abstract events, and the status that each is paired with, from the abstract machine's signature before we combine it with the concrete signature. We use the domain anti-restriction operator $\ndres$ to express this, where for any set $S$ and function $T$, we have

$$S\ndres T = \{x\mapsto y \mid x \mapsto y \in T \land x \notin S\}$$

In order to illustrate this signature extraction in practice, Figure <ref> contains the signature that was extracted, using these functions from  in Figure <ref>. Notice how the variables and events in the signature include those from the abstract machine,  in Figure <ref> (lines 8–29), and the constant from the context (lines 1–7) has been included as a $0$-ary operator using the  interface. We note that, internally,  distinguishes typing and non-typing invariants and we have used the typing invariants on lines 7–9 of Figure <ref> and line 13 of Figure <ref> to infer the types of the variables, and we assume an appropriate
mapping to types in .

$\Sigma_{\texttt{m1}} = \langle S, \Omega, \Pi, E, V \rangle$
$S = \{\mathbb{N}\}$,
$\Omega = \{0:\mathbb{N},d:\mathbb{N}\}$,
$\Pi = \{>:\mathbb{N}\times\mathbb{N}\}$,
$E = \{(\texttt{Init} \mapsto \texttt{ordinary}), (\texttt{ML\_in} \mapsto \texttt{ordinary}), (\texttt{ML\_out} \mapsto \texttt{ordinary})$,
$(\texttt{Il\_in} \mapsto \texttt{convergent}), (\texttt{Il\_out} \mapsto \texttt{convergent})\},$
$V = \{\texttt{n:}\mathbb{N}, \texttt{a:}\mathbb{N}, \texttt{b:}\mathbb{N}, \texttt{c:}\mathbb{N}\}$

An example of the signature extraction: this is the result of applying the functions from Figure <ref> to the Event-B machine specification of  in Figure <ref>.

Once the environment has been formed, we can then define a systematic translation from specifications in Event-B to structured specifications over . We take a bottom-up approach to this translation which is comprised of two parts.

* The first mapping (in Figure <ref>) that we define is from the Event-B infrastructure sentences (invariants, variants, events and axioms) to sentences over  (for invariants, variants and events) and sentences over  (for axioms) in Section <ref>.

* The second mapping (in Figure <ref>) that we provide is from the superstructure components of an Event-B specification to structured specifications over  (for machines) and structured specifications over  (for contexts) in Section <ref>.

\bullet & \mathbb{S}_\Sigma: & MachineBody \rightarrow Sen_{{\iEVT}}(\Sigma)
\Comment{Build sentences from a machine body}\\[2pt]
&\mathbb{S}_\Sigma & \left\llbracket\begin{array}{l}
\texttt{variables }  v_1, \ldots, v_n \\
\texttt{invariants }  i_1,\ldots,i_n \\
\texttt{theorems }  t_1,\ldots,t_n \\
\texttt{variant }  n  \\
\texttt{events }  e_{init}, \ e_1,\ldots,e_n \\
\end{array}\right\rrbracket
\;=\;
\left(
\begin{array}{ll}
& \mathbb{I}_\Sigma\BR{i_1} \cup \ldots \cup \mathbb{I}_\Sigma\BR{i_n}
\\
\cup & \mathbb{V}_\Sigma \BR{n} \\
\cup & \mathbb{E}_\Sigma \BR{e_{init}} \\
\cup&  \mathbb{E}_\Sigma\BR{e_1} \cup \ldots \cup \mathbb{E}_\Sigma\BR{e_n}
\end{array}\right)\\
\\
\bullet & \mathbb{I}_\Sigma: & LabelledPred \rightarrow Sen_{{\iEVT}}(\Sigma)
\Comment{Invariant sentences}\\[2pt]
&\mathbb{I}_\Sigma &\BR{i} \;=\; \{\langle \BR{e},\;
\mathtt{F.and}(\mathbb{P}_\Sigma\BR{i}, \mathtt{F.}\iota (\Sigma.V)(\mathbb{P}_\Sigma\BR{i}))\rangle \mid e \in dom(\Sigma.E)\} \\
\\
\bullet & \mathbb{V}_\Sigma: & Expression \rightarrow Sen_{{\iEVT}}(\Sigma)
\Comment{Variant can't increase for non-ord.\ events}\\[2pt]
&\mathbb{V}_\Sigma &\BR{n}
\;=\;
\begin{array}[t]{lr@{\;\mid\;}l}
& \{\langle \BR{e},\;
\mathtt{F.lt}(\mathtt{F.}\iota(\Sigma.V)(\mathbb{T}_\Sigma \BR{n}), \mathbb{T}_\Sigma \BR{n}) \rangle & (e \mapsto \mathtt{convergent}) \in \Sigma.E\} \\
\cup & \{\langle \BR{e},\;
\mathtt{F.leq}(\mathtt{F.}\iota(\Sigma.V) (\mathbb{T}_\Sigma\BR{n}), \mathbb{T}_\Sigma \BR{n})\rangle & (e \mapsto \mathtt{anticipated}) \in \Sigma.E\}
\end{array}\\
\\

\bullet & \mathbb{E}_\Sigma: & InitEvent \rightarrow Sen_{{\iEVT}}(\Sigma)
\Comment{Initial event: get sentences from actions}\\[2pt]
&\mathbb{E}_\Sigma& \left\llbracket\begin{array}{l}
\texttt{event Initialisation}    \\
\texttt{status ordinary}   \\
\texttt{then } act_1, \ldots, act_n\\
\texttt{end}\\
\end{array}\right\rrbracket
\;=\;
\{\langle \mathtt{Init},\; BA \rangle \}\\
&& where\\
&& \qquad BA \;=\; \mathtt{F.and}(\mathbb{P}_\Sigma\BR{act_1},\ldots,\mathbb{P}_\Sigma\BR{act_n}) \\
\\

\end{array}$

\bullet & \mathbb{E}_\Sigma: & Event \rightarrow Sen_{{\iEVT}}(\Sigma)
\Comment{Non-initial event: get sentences from event body}\\[2pt]
&\mathbb{E}_\Sigma& \left\llbracket\begin{array}{l}
\texttt{event } e   \\
\texttt{status} \  s   \\
\texttt{refines } e_1, \ldots, e_n \\
\texttt{end}\\
\end{array}\right\rrbracket
\;=\;
\{\langle \BR{e},\; \mathbb{F}_\Sigma\BR{ebody} \rangle \}\\
\\
\bullet & \mathbb{F}_\Sigma: & EventBody \rightarrow \Sigma\textit{-formula}
\Comment{Build a {\iFOPEQ} formula for an event definition}\\[2pt]
&\mathbb{F}_\Sigma & \left\llbracket\begin{array}{l}
\texttt{any} \  p_1, \ldots, p_n  \\
\texttt{where} \ grd_1,\ldots, grd_n   \\
\texttt{with} \ w_1,\ldots, w_n \\
\texttt{then} \ act_1,\ldots,act_n \\
\end{array}\right\rrbracket
\;=\;
\begin{array}[t]{l}
\mathtt{F.exists} (p,\; \mathtt{F.and}(G, W, BA))\\[3pt]
\qquad\Comment{Formula is existentially quantified }\\
\qquad \CommentLN{over event parameters $p$}\\
\end{array}\\
&& where\\
&& \qquad p \;=\; \langle \BR{p_1}, \ldots, \BR{p_n} \rangle \Comment{List of parameters}\\
&& \qquad G \;=\; \mathtt{F.and}(\mathbb{P}_\Sigma\BR{grd_1},\ldots,\mathbb{P}_\Sigma\BR{grd_n}) \Comment{Guards}\\
&& \qquad W \;=\; \mathtt{F.and}(\mathbb{P}_\Sigma\BR{w_1} ,\ldots,\mathbb{P}_\Sigma\BR{w_n}) \Comment{Witnesses}\\
&& \qquad BA \;=\; \mathtt{F.and}(\mathbb{P}_\Sigma\BR{act_1},\ldots,\mathbb{P}_\Sigma\BR{act_n}) \Comment{Actions}\\
\\
\bullet & \mathbb{S}_\Sigma:& ContextBody \rightarrow Sen_{{\iFOPEQ}}(\Sigma)
\qquad \Comment{Context: get {\iFOPEQ} sentences from axioms}\\[2pt]
&\mathbb{S}_\Sigma & \left\llbracket\begin{array}{l}
\texttt{sets } s_1,\ldots,s_n \\
\texttt{constants } c_1, \ldots, c_n\\
\texttt{axioms }  a_1,\ldots,a_n  \\
\texttt{theorems } t_1,\ldots,t_n  \\
\end{array}\right\rrbracket
\;=\;
\{\mathbb{P}_\Sigma \BR{a_1}, \ldots, \mathbb{P}_\Sigma \BR{a_n} \}
\\
\end{array}$

The semantics for the Event-B infrastructure sub-language is provided by translating them into set of sentences.
For machines we generate sentences over , denoted $Sen_{{\iEVT}}(\Sigma)$, while for contexts we generate sentences over , denoted $Sen_{{\iFOPEQ}}(\Sigma)$. We use the interface operations and functions described in Figure <ref> throughout this translation.

§.§ Defining the Semantics of Event-B Infrastructure Sentences

In this section, we define a translation from Event-B infrastructure sentences to sentences over . We translate the axiom sentences that are found in Event-B contexts to sentences over  as they form part of the underlying Event-B mathematical language as shown in Figure <ref>. We refer the reader to Section <ref>, where we described how to translate Event-B variants, invariants and events into -sentences, and the equations described here mirrors this translation.

We define an overloaded meaning function, $\mathbb{S}_\Sigma$, for
specifications in Figure <ref>. $\mathbb{S}_\Sigma$ takes
as input a specification and returns a set of sentences over
($Sen_{{\iEVT}}(\Sigma)$) for machines and a set of sentences over
($Sen_{{\iFOPEQ}}(\Sigma)$) for contexts. When applying
$\mathbb{S}_\Sigma$ to a machine (resp. context) we also define
functions for processing invariants, variants and events
(resp. axioms). These are given by $\mathbb{I}_\Sigma,
\mathbb{V}_\Sigma$ and $\mathbb{E}_\Sigma$. Axioms are predicates that
can be translated into closed -formulae using the function
$\mathbb{P}_\Sigma$ which is defined in the interface in Figure

Given a list of invariants $i_1, \ldots, i_n$ we define the function
$\mathbb{I}_\Sigma$ in Figure <ref>. Each invariant, $i$,
is a LabelledPred from which we form the open
\BR{i}))$. Each invariant sentence is paired with each event name in
the signature to form the set $\{ \langle e,
\mathtt{F.and}(\mathbb{P}_\Sigma\BR{i},\mathtt{F.}\iota(\Sigma.V)(\mathbb{P}_\Sigma
\BR{i}))\rangle \mid e \in dom(\Sigma.E)\}$ and this ensures that the
invariant is applied to all events when evaluating the satisfaction

The use of conjunction here for invariants ($\mathtt{F.and}$) rather
than implication may seem an unusual choice.  Typically (e.g. Abrial's
INV proof obligation, <cit.>), one demands
that if the invariant holds in the before-state then it should also
hold in the after-state.  However, since our sentences are effectively
indexed by events, and our semantics are stratified over events, we
are always working in a context where a given event has occurred.
Thus, in this (localised) context, we specify that the invariant must hold
in both the before and after states.  Since separate
sentences are conjoined when grouped, using an implication here would
also allow undesirable models when such sentences are combined.

Given a variant expression $n$, we define the function $\mathbb{V}_\Sigma$ in Figure <ref>. The variant is only relevant for specific events so we pair it with an event name in order to meaningfully evaluate the variant expression. An event whose status is  must strictly decrease the variant expression [2]. An event whose status is  must not increase the variant expression. This expression can be translated into an open -term using the function $\mathbb{T}_\Sigma$ as described in Figure <ref>. From this we  form a formula based on the status of the event(s) in the signature $\Sigma$ as described in Section <ref>. Event-B machines are only permitted to have one variant [3].

In Figure <ref> we define the function $\mathbb{E}_\Sigma$ to process a given event definition. Event guard(s) and witnesses are predicates that can be translated via $\mathbb{P}_\Sigma$ into open -formulae denoted by $G$ and $W$ respectively in Figure <ref>. In Event-B, actions are interpreted as before-after predicates e.g.  is interpreted as . Therefore, actions can also be translated via $\mathbb{P}_\Sigma$ into open -formulae denoted by $BA$ in Figure <ref>. Thus the semantics of an $EventBody$ definition is given by the function $\mathbb{F}_\Sigma$ which returns the formula $\mathtt{F.exists} (p, \mathtt{F.and}(G, W, BA))$ where $p$ is a list of the event parameters.

A context can exist independently of a machine and is written as a specification over . Thus, we translate an axiom sentence directly as a -sentence which is a closed $\Sigma$-formula using the function $\mathbb{P}_\Sigma$ given in Figure <ref>. Axiom sentences are closed -formulae (elements of $Sen_{{\iFOPEQ}}(\Sigma)$) which are interpreted as valid sentences in  using the comorphism $\rho$.

Figure <ref> describes our equations for the Event-B infrastructure constructs.  Next we show the relevant equations for the Event-B superstructure constructs.

§.§ Defining the Semantics of Event-B Superstructure Sentences

Based on the syntax defined in Figure <ref> we have
identified the core constructs that form the Event-B superstructure

* A context  other contexts

* A machine  contexts and
another (more abstract) machine

* An individual event  other events from the
abstract machine

In this section, we define a semantics for the Event-B superstructure language using specification-building operators. In Figure <ref> we define the  function $\mathbb{B}$ to translate Event-B specifications written using the superstructure language to structured specifications over  that use the specification-building operators defined in the theory of institutions <cit.>.
We translate a specification as described by Figure <ref> into a structured specification over the institution .

The semantics of an Event-B specification $SP$ are given by
$\mathbb{B}\BR{SP}\xi$, where $\xi = \mathbb{D}\BR{SP}\xi_0$ is the environment defined by Figure

\bullet & \mathbb{B}:& Specification \rightarrow Env \rightarrow \lvert\textbf{Spec}\rvert^*
\Comment{Process specifications in an environment,}\\[2pt]
&\mathbb{B}& \BR{\langle~\rangle}\;  \xi \;=\; \langle~\rangle
\CommentLN{build a list of structured specifications}\\
&\mathbb{B}& \BR{hd :: tl}\;  \xi
\;=\;
(\mathbb{B}\; \BR{hd}\; \xi) :: (\mathbb{B}\; \BR{tl}\; \xi)\\
\vspace{5pt}\\
\bullet & \mathbb{B}:& Machine \rightarrow Env \rightarrow \lvert\textbf{Spec}_{\iEVT}\rvert
\Comment{Build an {\iEVT} structured specification for one machine}\\[2pt]
\left\llbracket\begin{array}{l}
\texttt{machine } m \\
\texttt{refines }  a \\
\texttt{sees }  ctx_1, \ldots, ctx_n \\
mbody \\
\texttt{end}\\
\end{array}\right\rrbracket\; \xi
\;=\;
\begin{array}{l}
\left\langle\begin{array}{l}
\Sigma, \;
\left[\begin{array}{l}
\SPEC{\BR{m}}{\iEVT} \\
\quad\CommentNF{Include contexts using the comorphism $\rho$:}\\
\quad(\BR{ctx_1} \mathtt{\;\ikw{and}\;} \ldots \mathtt{\;\ikw{and}\;} \BR{ctx_n}) \mathtt{\;\ikw{with}\;} \rho \\
\quad\Comment{Sentences from the refined machine (if any):}\\
\quad(\mathtt{\ikw{and}\;} \mathbb{A}_{\Sigma} \BR{mbody}\BR{a} \xi) \\
\mathtt{\ikw{then}} \\
\quad \mathbb{S}_\Sigma\BR{mbody}\\
\end{array}\right] \\
\end{array}\right\rangle\\[2pt]
\quad
where \ \Sigma = \xi\BR{m}. \\
\end{array}\\
\\
\bullet & \mathbb{A}_\Sigma: & MachineBody \rightarrow EventName \rightarrow Env \rightarrow |\mathbf{Spec}_{\iEVT}|
\Comment{Extract any relevant specification from }\\
&& \CommentLN{the refined (abstract) machine}\\[-2ex]
&\mathbb{A}_\Sigma& \left\llbracket\begin{array}{l}
\texttt{variables }  v_1, \ldots, v_n \\
\texttt{invariants }  i_1,\ldots,i_n \\
\texttt{theorems }  t_1,\ldots,t_n \\
\texttt{variant }  n  \\
\texttt{events }  e_{init}, \ e_1,\ldots,e_n \\
\end{array}\right\rrbracket \BR{a}\; \xi
\;=\;
\begin{array}[t]{l}
\mathbb{I}_\Sigma\BR{i_1} \mathtt{\;\ikw{and}\;}\ldots \mathtt{\;\ikw{and}\;}\mathbb{I}_\Sigma\BR{i_n} \\
\mathtt{\ikw{and}\;}
\mathbb{R}_\Sigma\BR{e_1}\BR{a}\xi
\mathtt{\;\ikw{and}\;}\ldots \mathtt{\;\ikw{and}\;}\mathbb{R}_\Sigma\BR{e_n}\BR{a}\xi\\[3pt]
\Comment{Conjoin sentences from each event definition}\\
\end{array}\\
\\
\end{array}$

\bullet & \mathbb{R}_\Sigma: & Event\rightarrow EventName \rightarrow Env \rightarrow |\mathbf{Spec}_{\iEVT}|
\Comment{Extract specification from one refined event}\\[2pt]
\left \llbracket \begin{array}{l}
\texttt{event } e_c   \\
\texttt{status} \  s  \\
\texttt{refines} \  e_{1}, \ldots, e_{n}  \\
\texttt{end}\\
\end{array} \right \rrbracket\; \BR{a}\; \xi
\;=\;
\begin{array}{l} \mathtt{let}\\
\qquad \Sigma_a = \xi \BR{a},
\qquad\Comment{Signature of abstract machine}\\
\qquad \CommentNF{Use $\Sigma_h$, $\sigma_h$ to select only refined events:} \\
\qquad \Sigma_h = \langle \Sigma_a.S,\, \Sigma_a.\Omega, \,\Sigma_a.\Pi,\\
\qquad \hfill \{\BR{e_1}, \ldots, \BR{e_n}\} \lhd \Sigma_a.E ,\, \Sigma_a.V \rangle,\\
\qquad \sigma_h : \Sigma_h \hookrightarrow \Sigma_a,\\
\qquad \CommentNF{Use $\sigma_m$ to reassign refined event sentences to $e_c$:}\\
\qquad \sigma_m: \Sigma_h \rightarrow \Sigma\\
\qquad \sigma_m = \left\langle\begin{array}{l}
\Sigma_h.S \hookrightarrow\Sigma.S,\;
\Sigma_h.\Omega \hookrightarrow\Sigma.\Omega,
\Sigma_h.\Pi\hookrightarrow\Sigma.\Pi,\\
\Sigma_h.E \mapsto \{\BR{e_c}\} \lhd \Sigma.E,\\
\Sigma_h.V \hookrightarrow\Sigma.V
\end{array}\right\rangle\\
\mathtt{in }\\
\qquad (\BR{a} \mathtt{\;\ikw{hide\;via}\;} \sigma_h)\mathtt{\;\ikw{with}\;} \sigma_m.
\end{array}\\
\\
\bullet & \mathbb{B}:& Context \rightarrow Env \rightarrow \lvert\textbf{Spec}_{\iFOPEQ}\rvert
\Comment{Build a {\iFOPEQ} structured specification for one context}\\[2pt]
&\mathbb{B} & \left\llbracket\begin{array}{l}
\texttt{context } ctx \\
\texttt{extends } ctx_1,\ldots,ctx_n \\
\texttt{end}
\end{array}\right\rrbracket \xi
\;=\;
\begin{array}{l}
\left\langle\begin{array}{l}
\Sigma, \;
\left[\begin{array}{l}
\SPEC{\BR{ctx}}{\iFOPEQ} \\
\qquad \BR{ctx_1} \mathtt{\;\ikw{and}\;} \ldots \mathtt{\;\ikw{and}\;}  \BR{ctx_n}\\
\mathtt{\ikw{then}}\\
\qquad \mathbb{S}_\Sigma \BR{cbody}
\end{array}\right]\\
\end{array}\right\rangle \\
\\[-1.75ex]
\qquad where \ \Sigma = \xi \BR{ctx}.
\end{array}
\end{array}$
The semantics for the Event-B superstructure sub-language is defined by translating them into structured specifications over  using the function $\mathbb{B}$ and the specification-building operators defined in the theory of institutions (Table <ref>). Note that $\textbf{Spec}$ denotes the category of specifications as per <cit.>.

The construct that enables a context to extend others is used in Event-B to add more details to a context. Since a context in Event-B only refers to elements of the  component of an  signature it is straightforward to translate this using the specification-building operator then.
As outlined in Table <ref>, then is used to enrich the signature with new sorts/operations etc. <cit.>.

A context can be extended by more than one context. In this case the resulting context contains all constants and axioms of all extended contexts and the additional specification of the extending context itself [3].
To give a semantics for context extension using the specification-building operators we and all extended contexts and use then to incorporate the extending context itself.
The specification-building operator and takes the sum of two specifications that can be written over different signatures (Table <ref>).
It is the most straightforward way to combine specifications over different signatures <cit.>.

In Event-B, a machine  one or more contexts. This construct is used to add a context(s) to a machine so that the machine can refer to elements of the context(s). We know that the relationship between  and  is that of an institution comorphism (Definition <ref>) [18]. This enables us to directly use -sentences, as given by the context in this case, in an  specification. We use the specification-building operation with $\rho$ which indicates  translation by an institution comorphism $\rho$ <cit.>. The resulting machine specification is heterogeneous as it links two institutions,  and , by the institution comorphism.

An Event-B machine can refine at most one other machine and there are two types of machine refinement: superposition and data refinement [3]. The specification-building operator, then, can account for both of these types of refinement because either new signature components or constraints on the data (gluing invariants) are added to the specification. In Figure <ref> the function $\mathbb{A}_{\Sigma}$ is used to process the events in the concrete machine which refine those in the abstract machine.

Event refinement in Event-B is superposition refinement [3]. By superposition refinement all of the components of the corresponding abstract event are implicitly included in the refined version. This approach is useful for gradually adding more detail to the event. In , we have not prohibited multiple definitions of the same event name. When there are multiple definitions we combine them by taking the conjunction of their respective formulae which will constrain the model. As mentioned above, when refining an abstract machine we use the function $\mathbb{A}_{\Sigma}$, in Figure <ref> to process the events in the concrete machine which refine those in the abstract machine. $\mathbb{A}_{\Sigma}$ in turn calls the function $\mathbb{R}_{\Sigma}$ (Figure <ref>).

$\mathbb{R}_{\Sigma}$ restricts the event component of the abstract
machine signature to those events contained in the
clause of the event definition using domain restriction
($\dres$). $\mathbb{A}_{\Sigma}$ also extracts the invariant sentences
from the abstract machine. This new signature is included in the
abstract machine via the signature morphism $\sigma_h$. We then form
the signature morphism $\sigma_m$ by letting it be the identity on the sort,
operation, predicate and variable components of $\Sigma_h$.
For events, $\sigma_m$ maps each of the abstract event signature components that are being refined by the concrete event $e_c$ to the signature component corresponding to $e_c$. The resulting specification uses hide via and with to apply these signature morphisms ($\sigma_h$ and $\sigma_m$) correctly. Note that we could have used the reveal specification-building operator rather than hide via to achieve the same result <cit.>.

Thus, we have formalised an institution-based  semantics for the three layers of the Event-B language.
In previous empirical work, we discovered that the Event-B language is lacking a well-defined set of modularisation constructs [19]. It is clear that the specification-building operators available in the theory of institutions can provide a solution to this. We validate our  semantics and show how these specifications can be modularised using the specification-building operators in the next sections.

§ THE SEMANTICS IN ACTION: A WORKED EXAMPLE

In order to validate our  semantics we developed a tool to take Event-B specifications and generate the corresponding -specifications, following the definitions given in Section <ref>.
The tool is called  and takes as input an Event-B specification in the XML format used by , and generates as output the -specifications, syntactically sugared in a -like notation.
is written in Haskell [68], a choice that allows our code to closely mirror the function definitions, and is compatible with the  code-base.
To illustrate the approach, Figure <ref> shows the
associated Haskell code snippet of the $\mathbb{F}$ function from
Figure <ref>. The reader  need only refer back to the
definition of $\mathbb{F}_\Sigma$ in Figure <ref> to see their correspondence.

bbEventDefines ::[(Ident, Ident)]-> [EventDef] -> [Sentence]
bbEventDefines xx' evtList =
let pp eBody = (eany eBody)
gg eBody = F.and (ewhere eBody)
ww eBody = F.and (ewith eBody)
ba eBody = F.and (ethen eBody)
bbEvent eBody = (F.exists (xx' ++(pp eBody)) (F.and [gg eBody, ww eBody, ba eBody]))
bbEventDef evt = (Sentence (ename evt) (bbEvent (ebody evt)))
in (map bbEventDef evtList)

The Haskell implementation of the $\mathbb{F}$ function from Figure <ref> as applied to a list of Event-B event definitions.

§.§ The Abstract Model

We illustrate the use of  using the cars on a bridge example as introduced in Section <ref>. This Event-B specification has three refinement steps, resulting in four machines and three contexts. The final refinement step results in quite a large specification and so we omit it here but more details can be found in [16].
We present the resultant -specification corresponding to each of the first two refinement steps.

Figure <ref> introduced an abstract Event-B specification and using our  translator tool we obtain the corresponding -specification that is presented in Figure <ref>.

Lines 1–5 This is a -specification that describes the context from Figure <ref>. Note that  is a sub-logic of  [47] and we use  in its place here because it is available in  [46].  The constant $d$ is represented as an operation of the appropriate type and the non-typing axioms are included as predicates. This is achieved via the function $\mathbb{P}$ that was defined in the  interface (Figure <ref>).

Lines 6–20 This is the -specification that is generated corresponding to the abstract machine in Figure <ref> (lines 8–29). The machine variable, $n$, is represented as an operation and the context specification is included using the then specification-building operator on lines 7 and 8. This corresponds to the application of the function $\mathbb{B}$ (Figure <ref>) to the superstructure components of the machine.

With regard to the infrastructure translation described in Figure
<ref>, note that the invariant and event sentences have
been syntactically sugared in order to simplify the notation.  In
this and future examples, we use
thenAct in place of the then Event-B keyword to
distinguish it from the then specification-building operator.

§.§ The First Refinement

In Figure <ref> we presented a refinement of the abstract specification that was introduced in Figure <ref>. Using our  translator tool, we obtain the -specification corresponding to this machine as shown in Figure <ref>.

Lines 1–3 The application of $\mathbb{B}$ to the
and  clauses of Figure <ref> (lines 2–3) results in the application of the specification-building operators (and, then) to include the abstract machine and context specifications into the generated -specification.

Lines 4–9 The new variables and (non-theorem) invariants are included as operations and predicates respectively. For readability, we use a simple notation for the variant expression on line 9. The reader should understand that the semantics of this is evaluated as described in Figure <ref>.

Lines 10–31 $\mathbb{R}_{\Sigma}$ returns ( $\sigma_h$)  $\sigma_m$ for each refined event. The event names have remained the same during event refinement in this example, and since events with the same name are implicitly merged we can omit this notation here.

sort $\mathbb{N}$
ops  d:$\mathbb{N}$
.  d $> 0$

ops  n:$\mathbb{N}$
.  $n\mathbin{\leq}d$

thenAct  n := 0
when $n<d$
thenAct  n := n+1
when $n>0$
thenAct  n := n-1

A structured specification in the  institution (syntactically
sugared)  as generated by .  This specification corresponds
to the Event-B specification of the abstract machine given in Figure

m0 and cd
ops  a:$\mathbb{N}$
.  $n=a+b+c$
$a=0 \lor c=0$
variant $2*a+b$
thenAct  a := 0
b := 0
c := 0
when $a+b<d$
thenAct a := a+1
when  $a>0 $
thenAct a := a-1
b := b+1
when $0<b $
thenAct b := b-1
c := c+1
when  $c>0$
thenAct  c := c-1

An  specification corresponding to the results of the
first refinement step, as represented by the Event-B specification in
Figure <ref>.

red, green
axm4Color = {green,red}
axm3green ≠red

cd, Color
a, b, c, ml_tl, il_tl,
il_pass, ml_pass
inv1ml_tl ∈{red,green}
inv2il_tl ∈{red,green}
inv3ml_tl=green ⇒c=0
inv12ml_tl=green ⇒a+b+c<d
inv4il_tl=green ⇒a=0
inv11il_tl=green ⇒b>0
inv8ml_tl=red ⇒ml_pass=1
inv9il_tl=red ⇒il_pass=1
inv5il_tl=red ml_tl=red
thm20≥a ⇒a=0 theorem
thm30≥b ⇒b=0 theorem
thm40≥c ⇒c=0 theorem
thm5¬(d≤0) theorem
thm6b+1≥d ¬(b+1=d)
$ \Rightarrow \lnot(b<d)$ theorem
thm7b≤1 ¬(b=1)
$ \Rightarrow \lnot(b>0)$ theorem
thm1(ml_tl= green a+b+1<d)
$\lor (ml\_tl=green \land a+b+1=d)$
$\lor (il\_tl=green \land b>1)$
$\lor (il\_tl=green \land b=1)$
$\lor (ml\_tl=red \land a+b<d$
$\land c=0 \land il\_pass=1)$
$\lor (il\_tl=red \land 0<b \land a=0 $
$\land ml\_pass=1)$
$\lor 0<a \lor 0<c$ theorem
ml_pass + il_pass
then act2a := 0
act3b := 0
act4c := 0
act1ml_tl := red
act5il_tl := red
act6ml_pass := 1
act7il_pass := 1

when grd1ml_tl = green
then act1a := a+1
act2ml_pass := 1
when grd1ml_tl=green
then act1a := a+1
act2ml_tl := red
act3ml_pass := 1
when grd1il_tl=green
then act1b := b-1
act2c := c+1
act3il_pass := 1
when grd1il_tl=green
then act1b := b-1
act2il_tl := red
act3c := c+1
act4il_pass := 1
when grd1ml_tl=red
then act1ml_tl := green
act2il_tl := red
act3ml_pass := 0
when grd1il_tl=red
then act1il_tl := green
act2ml_tl := red
act3il_pass := 0
when grd110<a
then act11a := a-1
act12b := b+1
when grd10<c
then act1c := c+1

An Event-B specification of a machine  that
refines the Event-B machine in Figure <ref> by adding new
events  and . The
context  on lines 1–8 adds a new data type which is
used by the  and  traffic light variables.

sorts  Color
ops  red: Color
green: Color
.  Color = {green,red}
green $\neq$ red

m1 and cd and COLOR and
(m1  hide via  $\sigma_{h_{\texttt{ ML\_out}}})$ with $ \sigma_{m_{\texttt{ ML\_out}\mapsto\texttt{ML\_out1}}}$ and
(m1  hide via  $\sigma_{h_{\texttt{ ML\_out}}})$ with $ \sigma_{m_{\texttt{ ML\_out}\mapsto\texttt{ML\_out2}}}$ and
(m1  hide via  $\sigma_{h_{\texttt{ IL\_out}}})$ with $ \sigma_{m_{\texttt{ IL\_out}\mapsto\texttt{IL\_out1}}}$ and
(m1  hide via  $\sigma_{h_{\texttt{ IL\_out}}})$ with $ \sigma_{m_{\texttt{ IL\_out}\mapsto\texttt{IL\_out2}}}$
ops  ml_tl : {red,green}
il_tl :  {red,green}
il_pass :  {0,1}
ml_pass :  {0,1}
.  ml_tl=green $\Rightarrow$ c=0
ml_tl=green $\Rightarrow$ a+b+c<d
il_tl=green $\Rightarrow$ a=0
il_tl=green $\Rightarrow$ b>0
ml_tl=red $\Rightarrow$ ml_pass=1
il_tl=red $\Rightarrow$ il_pass=1
il_tl=red $\lor$ ml_tl=red
variant  ml_pass+il_pass
thenAct  a := 0
b := 0
c := 0
ml_tl := red
il_tl := red
ml_pass := 1
il_pass := 1
when  ml_tl=green
thenAct  a := a+1
ml_pass := 1

when  ml_tl=green
thenAct  a := a+1
ml_tl := red
ml_pass := 1
when  il_tl=green
thenAct  b := b-1
c := c+1
il_pass := 1
when  il_tl=green
thenAct  b := b-1
il_tl := red
c := c+1
il_pass := 1
when  ml_tl=red
thenAct  ml_tl := green
il_tl := red
ml_pass := 0
when  il_tl=red
thenAct  il_tl := green
ml_tl := red
il_pass := 0
when  0<a
thenAct  a := a-1
b := b+1
when  0<c
thenAct c := c-1

A structured specification in the  institution corresponding to
the Event-B specification of Figure <ref>, representing the
results of the second refinement step.

§.§ The Second Refinement

Figure <ref> contains an Event-B specification that shows the
second refinement step, which adds a substantial amount of new
behaviour to the specification. The first addition is a context (lines
1–8) containing colours which provide values for the new variables
( and ). These are used to control the
behaviour of a pair of traffic lights (line 12). The new variables
and  on line 13 are used to record whether or
not a car has passed through the mainland or island traffic light
respectively. The objective of these variables is to ensure that the
traffic lights do not change so rapidly that no car can pass through
them [2].  Events for these lights were added
to the machine and the current events were modified to account for
this behaviour. In particular, each of the abstract events
( and  in Figure <ref>) are
refined by two events (, ,
and  in Figure <ref>).

As can be seen from Figure <ref>, there is a good degree of
repetition in the Event-B specification resulting from common cases
for the numeric variables.  These can be represented much more
succinctly as a structured specification in our institution as shown in Figure

Lines 1–7 This  specification specifies the new data type $\texttt{Color}$. This corresponds to the context described in the Event-B model in Figure <ref>.

Lines 8–14 The superstructure component of the translation includes the abstract machine (), and the contexts ( and ). In this case the names of the events are changed in the refinement step. The event  is decomposed into the events  and . The event  follows a similar decomposition into  and . We account for this refinement using the signature morphisms and specification-building operators on lines 10–13. We have not explicitly described these signature morphisms but their functionality should be obvious from their respective subscripts.

Line 26 As before, we use a simple variant notation for the variant expression.

Lines 27–83 The events are translated as before for the remainder of the specification.

This example illustrates the use of  as a means for bridging
the gap between the  and  software eco-systems. The
source code for  along with more examples of its use can be found on our git repository[<https://github.com/mariefarrell/EB2EVT.git>].

§ ENHANCED REFINEMENT AND MODULARISATION IN

Our formalisation of Event-B in terms of the theory of institutions offers a number of benefits. In this section, we provide a discussion of refinement in this setting and how we can exploit the use of specification-building operators for modularisation of Event-B specifications.

§.§ Representing Refinement Explicitly

As is evidenced by our running example and Section <ref>, refinement is a central aspect of the Event-B methodology, therefore any formalisation of Event-B must be capable of capturing refinement. The theory of institutions equips us with a basic notion of refinement as model-class inclusion where the class of models of a specification contains the models that satisfy the specification. We formally define what is meant by model-class in Definition <ref>.

For any $\Phi \subseteq\mathbf{Sen}(\Sigma)$ of $\Sigma$-sentences, the class $Mod_{\Sigma}(\Phi) \subseteq\lvert\mathbf{Mod}(\Sigma)\rvert$ of models of $\Phi$ is defined as the class of all $\Sigma$-models that satisfy all the sentences in $\Phi$.

Note that we omit the $\Sigma$ subscript where the signature is clear from the context.
With regard to institution-theoretic refinement, the class of models of the concrete specification is a subset of the class of models of the abstract specification <cit.>.

We consider two cases: (1) when the signatures are the same and (2) when the signatures are different. In the case where the signatures are the same, refinement is denoted as:

$SP_A \sqsubseteq SP_C \quad\iff\quad Mod(SP_C) \subseteq Mod(SP_A)$
where $SP_A$ is an abstract specification that refines ($\sqsubseteq$) to a concrete specification $SP_C$, $Mod(SP_A)$ and $Mod(SP_C)$ denote the class of models of the abstract and concrete specifications respectively. This means that, given specifications with the same signature, the concrete specification should not exhibit any model that was not possible in the abstract specification. This equates to the definition of general refinement outlined in [52, 53].

In terms of Event-B, data refinement is not supported in this way because it would involve a change of signature. Instead, refinement occurs between machines by strengthening the invariants and the guards but does not provide any new variables or events. In this case, the specification is made more deterministic by further constraining the invariants and guards. This increase in determinism is supported by the refinement calculi  [6, 7, 44, 45].

When the signatures are different and related by a signature morphism $\sigma: Sig[SP_A] \rightarrow Sig[SP_C]$ then we can use the corresponding model morphism in order to express refinement. This model morphism is used to interpret the concrete specification as containing only the signature items from the abstract specification. Here, refinement is the model-class inclusion of the models of the concrete specification restricted into the class of models of the abstract specification using the model morphism. In this case we write:

$$SP_A \sqsubseteq SP_C \quad\iff\quad Mod(\sigma)(SP_C) \subseteq Mod(SP_A)$$

where $Mod(\sigma)(SP_C)$ is the model morphism applied to the model-class of the concrete specification $SP_C$. This interprets each of the models of $SP_C$ as models of $SP_A$ before a refinement relationship is determined. Note that we could have alternatively represented this kind of refinement using the hide via specification-building operator to transform $SP_C$ into a specification over the signature $Sig[SP_A]$ using the appropriate morphism.

In this scenario, both data refinement and superposition refinement are supported directly in , since the refined or added variables and events can be removed, using a suitable model morphism as outlined above, before refinement is completed. Schneider et al. used a similar notion of hiding when they provided a CSP semantics for Event-B refinement [60].

ML_in $\mapsto$ ML_in, ML_out $\mapsto$ ML_out

ML_in $ \mapsto$ ML_in, ML_out $\mapsto$ ML_out1,
IL_in $ \mapsto$ IL_in, IL_out $\mapsto$ IL_out1

ML_in $\mapsto$ ML_in, ML_out $\mapsto$ ML_out2,
IL_in $\mapsto$ IL_in, IL_out $\mapsto$ IL_out2,
A specification in the  institution that explicitly
defines the refinement relationships between the abstract machine
and its two concrete refinements. Note that, for readability, we omit the status mappings since all statuses are  in this case and remain as so after signature morphism.

Figure <ref> uses the refinement syntax available in  to specify each of the refinement steps in the cars on a bridge example.  Note that this allows us to express the refinement as a separate entity, whereas in Event-B the refinement step is woven into the definition of the refined machine.
In Figure <ref>, lines 1–3 define the refinement step between the abstract specification  and the concrete specification m1. In this step the events are refined but no renaming or statuses are changed so it is very straightforward.
Lines 4–11 define the refinement step between the specification  and the concrete specification . There are two separate refinements ( and ) because the events  and  are split into two further events each as presented in Figure <ref>.

The example that we presented in this paper does not make use of data refinement in Event-B but if it did, it would also be possible to capture this kind of refinement in the -style notation above. An example of this was presented in our previous work [18].

§.§ Modularisation using Specification-Building Operators

During the evolution of the Event-B formalism from Classical-B, certain facilities for the reuse of machine specifications disappeared. These include the modularisation properties supplied by the keywords  and  which facilitated the use of an existing machine in other developments [62]. Since then there have been numerous attempts at regaining such modularisation features [63, 26, 25, 31, 12, 51]. Modularisation in Event-B does not require re-engineering the language in the same way as Object-Z or VVSL, but rather, modifications are made by building plugins for .

Modularisation, in terms of decomposition, in Event-B was first described by Abrial as the act of cutting a large system of events into smaller pieces that can each be refined independently of the others [4]. This offers the advantage of separation of concerns even though there still needs to be a link between the parts. The central idea is that the specifications constructed via decomposition and further refinement may be easily recombined resulting in a specification that could have been obtained without using any decomposition techniques in the first place. Three primary types of Event-B decomposition have been identified [31]. These are shared variable [1], shared event [12] and modularisation [35]. Another related approach is generic instantiation [4].

It is clear, from observations of industrial projects and the sheer volume of  plugins developed for modularisation in Event-B, that there is an underlying demand for modularisation [35, 31].
In previous work, we assembled and analysed a corpus of Event-B specifications in light of their metrics and the incidence of specification clones throughout the corpus [19]. This work supported the claim that the Event-B formal specification language is in need of a set of well-defined modularisation constructs and we postulated that the specification-building operators of the theory of institutions could fill this void.

We have used the specification-building operators throughout our definitions in Section <ref> as a way of naturally adding modularisation to these specifications and this shines through in the example that we have shown above. Notably, we can use these specification-building operators to further modularise the specifications in our illustrative example. In particular, the -specification in Figure <ref> could be further modularised as is illustrated in Figure <ref>.

cd then
ops n:$\mathbb{N}$
. n $\leq$ d

thenAct n := 0

datam0 then
ops a, b, c : $\mathbb{N}$
. n = a + b + c
a = 0 $\lor$ c = 0
variant 2$*$a+b
thenAct  a := 0
b := 0
c := 0

ops v1, v2 : $\mathbb{N}$
when v1 = 0
thenAct v2 := v2 + 1
when v1 > 0
thenAct v1 := v1 + 1

datam1 and m0 and
inout with {$\langle$out, ordinary$\rangle$ $\mapsto$ $\langle$ML_out, ordinary$\rangle$,
$\langle$in, ordinary$\rangle$ $\mapsto$ $\langle$ML_in, ordinary$\rangle$,
v1 $\mapsto$ c, v2 $\mapsto$ a} and
inout with {$\langle$out, ordinary$\rangle$ $\mapsto$ $\langle$IL_out, convergent$\rangle$,
$\langle$in, ordinary$\rangle$ $\mapsto$ $\langle$IL_in, convergent$\rangle$,
v1 $\mapsto$ a, v2 $\mapsto$ c}
when a + b < d
thenAct b:= b + 1
when 0 < b
thenAct b := b + 1

A structured specification in the  institution that is an even more
modular version of the structured specification in Figure <ref>.

Lines 1–20 The specifications  (lines 1–8) and  (lines 9–20) capture the data parts of the  and  specifications and their  events (see Figures <ref> and <ref> for correspondence).

Lines 21–30 Since the  and  events are quite similar, modulo renaming of variables, to the  and  events we construct the  specification. This defines an  (lines 24–26) and an  event (lines 27–29) using natural number variables  and  (introduced on line 22).

Lines 31–48 This is a modular specification of  that instantiates two copies of the  specification with the appropriate signature morphisms mapping the  event to  in the first instance and to  in the second. Correspondingly,  maps to  and then to . Further to this, the sentences after the then keyword (lines 40–48) add extra behaviour to these events that was not made explicit in the  specification.

This specification is evidently more modular than the original version by modelling the simple behaviour of coming in and going out in a separate specification and then instantiating it twice with the appropriate events and variables renamed. This kind of modularisation of specifications is currently not available in the Event-B formal specification language, but our  institution allows us to enhance Event-B with these powerful modularisation constructs.

As already mentioned, a number of plugins exist with the objective of providing modularisation features for Event-B. However, although all of these plugins offer some form of modularisation for Event-B specifications, it is not clear how specifications developed utilising more than one of these plugins could be combined in practice, or, if this is even possible.

§.§ Capturing Current Event-B Modularisation

In this subsection, we illustrate how the functionality of a selection
of the current  modularisation plugins can be captured
using the specification-building operators and parametrisation made
available in the theory of institutions using .
Most of these plugins embody a shared variable or shared event style
of modularisation (e.g
[63, 12, 35]), and this section
demonstrates how our semantics provides a theoretical foundation for
current modularisation approaches in Event-B.  A more thorough
analysis of the current modularisation approaches available in the
Platform can be found in [16].

§.§.§ Shared Variable and Shared Event Decomposition

Modularisation is straightforward when the events in a machine each
reference their own, separate set of variables.  However, the more common
situation is for events to share variables, as is illustrated by the
machine  at the top of Figures <ref> and <ref>.  In
machine , each of the three variables $\{\mathtt{v1}, \mathtt{v2}, \mathtt{v3}\}$ is
referenced by two different events (we have omitted the event status and
variable sorts from this example to increase clarity).  In each case
we wish to split machine  into two equivalent sub-machines  and
, and Figures <ref> and <ref> show two
different approaches to achieving this in Event B.

Figure <ref> illustrates the shared variable
approach, where an Event-B machine is decomposed into sub-machines
by grouping events which share the same variables
Since this may not produce a partition, the user must choose which
events to allocate to a sub-machine, e.g. in Figure <ref> we
allocate events  and  to sub-machine
and events  and  to sub-machine .
Since  and  both
refer to  in Figure <ref>, `external' events
and  are added to
abstractly describe the behaviour of the shared variable in the other

The shared variable decomposition of machine
into sub-machines  and . Here we
wish to partition machine  into two sets of events, as shown by
the dotted line.

(M hide via $ \sigma_1$)
with { e3 $\mapsto$ e3_e }
where $\sigma_1$ = { v1 $\mapsto$ v1, v2 $\mapsto$ v2, e1 $\mapsto$ e1,
e2 $\mapsto$ e2, e3 $\mapsto$ e3 }

(M hide via $ \sigma_2$)
with { e2 $\mapsto$ e2_e }