# Structured Types

From Event-B

Revision as of 16:03, 1 May 2009 by imported>WikiSysop (→Modelling 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 'C' with fields 'e' and 'f' (with type E and F respectively). Let us use the following syntax for this (not part of Event-B):

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

Now, given an element representing a record, we write for the 'e' component of structure