# Structured Types

## Contents

## 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 syntax for this (not part of Event-B syntax):

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:

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

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

## Constructing Structured Values

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

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:

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:

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

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

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

## 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 syntax for this (not part of Event-B syntax):

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

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:

The event extension mechanism means that this short form is the same as specifying the refined event as follows: