Structured Types

Modelling Structured Types

The Event-B mathematical language currently does not support a syntax for the direct definition of structured types such as records or class structures. Nevertheless it is possible to model structured types using projection functions to represent the fields/attributes. For example, suppose we wish to model a record structure R with fields e and f (with type E and F respectively). Let us use the following 'invented' syntax for this (not part of Event-B syntax):

$\begin{array}{lcl} \textbf{RECORD}~~~~ R &::& e\in E\\ && f \in F \end{array}$

We can model this structure in Event-B by introducing (in a context) a carrier set R and two functions e and f as constants as follows:

$\begin{array}{l} \textbf{SETS}~~ R\\ \textbf{CONSTANTS}~~ e,~ f\\ \textbf{AXIOMS}\\ ~~~~\begin{array}{l} e \in R \tfun E\\ f \in R \tfun F\\ \end{array} \end{array}$

The (constant) functions e and f are projection functions that can be used to extract the appropriate field values. That is, given an element $r\in R$ representing a record structure, we write $e(r)$ for the e component of r and $f(r)$ for the f component of r.

E and F can be any type definable in Event-B, including a type representing a record structure.

The approach to modelling structured types is based on a proposal by Evans and Butler [1].

Constructing Structured Values

Suppose we have a variable v in a machine whose type is the structure R defined above:

$\textbf{INVARIANT}~~ v\in R$

We wish to assign a structured value to v whose e field has some value e1 and whose f field has some value f1. This can be achieved by specifying the choice of an event parameter r whose fields are constrained by appropriate guards and assigning parameter r to the machine variable v. This is shown in the following event:

$Ev1 ~=\begin{array}[t]{l} \textbf{ANY}~~ r ~~\textbf{WHERE} \\ ~~~~ r \in R \\ ~~~~ e( r ) = e1 \\ ~~~~ f( r ) = f1 \\ \textbf{THEN} \\ ~~~~ v := r \\ \textbf{END} \end{array}$

If we only wish to update some fields and leave others changed, this needs to be done by specifying explicitly that some fields remain unchanged. This is shown in the following example where only the e field is modified:

$Ev2 ~=\begin{array}[t]{l} \textbf{ANY}~~ r ~~\textbf{WHERE} \\ ~~~~ r \in R \\ ~~~~ e( r ) = e1 \\ ~~~~ f( r ) = f(v) \\ \textbf{THEN} \\ ~~~~ v := r \\ \textbf{END} \end{array}$

If we don't care about the value of some field (e.g., f), we simply omit any guard on that field as follows:

$Ev3 ~= \begin{array}[t]{l} \textbf{ANY}~~ r ~~\textbf{WHERE} \\ ~~~~ r \in R \\ ~~~~ e( r ) = e1 \\ \textbf{THEN} \\ ~~~~ v := r \\ \textbf{END} \end{array}$

Sometimes we will wish to model a set of structured elements as a machine variable, e.g.,

$\textbf{INVARIANT}~~ vs\subseteq R$

We can add a structured element to this set using the following event:

$AddElement ~= \begin{array}[t]{l} \textbf{ANY}~~ r ~~\textbf{WHERE} \\ ~~~~ r \in R \\ ~~~~ e( r ) = e1 \\ ~~~~ f( r ) = f1 \\ \textbf{THEN} \\ ~~~~ vs := vs \cup \{r\} \\ \textbf{END} \end{array}$

Extending Structured Types

In a refinement we can introduce new fields to an existing structured type. Suppose R is defined in context C1 with fields e and f as before. For the refinement, suppose we wish to add a field g of type G to structured type R. Let us use the following invented syntax for this (not part of Event-B syntax):

$\begin{array}{l} \textbf{EXTEND~~ RECORD}~~ R ~~\textbf{WITH}~~ g\in G \end{array}$

This can be done by including the new field g as projection function on R in a context C2 (that extends C1). The new field is defined as follows:

$\begin{array}{l} \textbf{CONSTANTS}~~ g \\ \textbf{AXIOMS}\\ ~~~~\begin{array}{l} g \in R \tfun G \\ \end{array} \end{array}$

Above, we saw the AddElement event that adds a structured element to the set vs. We may want to specify a value for the new g field in the refinement of this event. Using the event extension mechanism, this can be achieved as follows:

$AddElement~= \begin{array}[t]{l} \textbf{EXTENDS}~~ AddElement \\ \textbf{WHEN} \\ ~~~~ g( r ) = g1 \\ \textbf{THEN} \\ ~~~~ skip \\ \textbf{END} \end{array}$

This is a form of superposition refinement where we add more data structure to the state by adding a new field to elements of the structured type R. In the above event we strengthen the specification by adding a guard using the event extension mechanism. The event extension mechanism means that this short form is the same as specifying the refined event as follows:

$AddElement ~= \begin{array}[t]{l} \textbf{REFINES}~~ AddElement \\ \textbf{ANY}~~ r ~~\textbf{WHERE} \\ ~~~~ r \in R \\ ~~~~ e( r ) = e1 \\ ~~~~ f( r ) = f1 \\ ~~~~ g( r ) = g1 \\ \textbf{THEN} \\ ~~~~ vs := vs \cup \{r\} \\ \textbf{END} \end{array}$

Sub-Typing

Extension, as described above, is used when adding new fields to a structured type as part of a refinement step. That is, at different abstraction levels, we may have different numbers of fields in a structured type.

Sometimes we wish to have different subtypes of a structure at the same abstraction level. We can achieve this by defining subset of the structure type and defining projection functions for those subsets only. For example suppose we define a message type that has sender and receiver fields as well as a message identifier. In our invented notation this would be:

$\begin{array}{lcl} \textbf{RECORD}~~~~ Message &::& sender\in Agent\\ && receiver \in Agent \\ && ident \in Ident \end{array}$

In Event-B this would be:

$\begin{array}{l} \textbf{SETS}~~ Message\\ \textbf{CONSTANTS}~~ sender,~ receiver, ident\\ \textbf{AXIOMS}\\ ~~~~\begin{array}{l} sender \in Message \tfun Agent\\ receiver \in Message \tfun Agent\\ ident \in Message \tfun Ident \end{array} \end{array}$

We wish to have two subtypes of message, request messages and confirmation messages. We define two subsets of Message as follows:

$\begin{array}{l} \textbf{CONSTANTS}~~ \textit{ReqMessage},~ \textit{ConfMessage}\\ \textbf{AXIOMS}\\ ~~~~\begin{array}{l} \textit{ReqMessage} \subseteq Message \\ \textit{ConfMessage} \subseteq Message \\ \end{array} \end{array}$

We require requests to have a product and an amount field and a confirmation to have a price field. In our invented notation this would be specified as follows:

$\begin{array}{l} \textbf{EXTEND~~ RECORD}~~ \textit{ReqMessage}~~\textbf{WITH}\\ ~~~~~~~~~~~~ product\in Product\\ ~~~~~~~~~~~~ amount\in \nat\\ \textbf{EXTEND~~ RECORD}~~ \textit{ConfMessage}~~\textbf{WITH}\\ ~~~~~~~~~~~~ price\in \nat\\ \end{array}$

In Event-B the additional fields are specified as projection functions on the relevant message subsets:

$\begin{array}{l} \textbf{CONSTANTS}~~ product,~ amount, price\\ \textbf{AXIOMS}\\ ~~~~\begin{array}{l} product \in \textit{ReqMessage} \tfun Product\\ amount \in \textit{ReqMessage} \tfun \nat\\ ~\\ price \in \textit{ConfMessage} \tfun \nat \end{array} \end{array}$

Typically we would require that the message subtypes are disjoint. In that case we would add and additional axiom:

$\begin{array}{l} \textbf{AXIOMS}\\ ~~~~\begin{array}{l} \textit{ReqMessage} \cap \textit{ConfMessage} ~=~ \emptyset \\ \end{array} \end{array}$

If we know that theee are no other subtypes besides requests and confirmations and they should be disjoint, then we can condense subset and disjointness axioms into a partitions axiom:

$\begin{array}{l} \textbf{AXIOMS}\\ ~~~~\begin{array}{l} partition(~ Message, ~\textit{ReqMessage},~ \textit{ConfMessage} ~) \end{array} \end{array}$

Suppose we have 2 variables representing request and confirmation channels repsectively:

$\begin{array}{l} \textbf{INVARIANT}~~ \\ ~~~~req\_channel \subseteq \textit{ReqMessage} \\ ~~~~\textit{conf\_channel} \subseteq \textit{ConfMessage} \end{array}$

The following Confirm event models an agent responding to request by issuing a confirmation message. The confirm event is enabled for the agent if there is a request message, req, whose receiver is that agent. The effect of the event is to chose a confirmation message, conf, whose fields are constrained with appropriate guards and adding that confirmation message to the confirmations channel:

$Confirm ~= \begin{array}[t]{l} \textbf{ANY}~~ req,~ conf, ~ agent ~~\textbf{WHERE} \\ ~~~~ req \in req\_channel \\ ~~~~ agent = receiver(req) \\ ~~~~ conf \in \textit{ConfMessage} \\ ~~~~ sender( conf ) = agent \\ ~~~~ receiver( conf ) = sender(req) \\ ~~~~ price(conf) = calculate\_price(~ product(req)\mapsto amount(req) ~) \\ \textbf{THEN} \\ ~~~~ \textit{conf\_channel} := \textit{conf\_channel} \cup \{conf\} \\ \textbf{END} \end{array}$