# Difference between revisions of "Structured Types"

From Event-B

Jump to navigationJump to searchimported>WikiSysop |
imported>WikiSysop |
||

Line 3: | Line 3: | ||

The Event-B mathematical language currently does not support a syntax for the direct definition of structured types such as records or class structures. | 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, | 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). | + | 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): | + | Let us use the following syntax for this (not part of Event-B syntax): |

<center> | <center> | ||

Line 16: | Line 16: | ||

</center> | </center> | ||

− | We can model this structure in Event-B by introducing (in a context) a set | + | We can model this structure in Event-B by introducing (in a context) a carrier set ''C'' and two |

− | functions | + | functions ''e'' and ''f'' as constants as follows: |

<center> | <center> | ||

Line 35: | Line 35: | ||

− | Now, given an element <math>c\in C</math> representing a record, we write | + | Now, given an element <math>c\in C</math> representing a record, we write ''e(c)'' for the ''e'' component of structure |

## Revision as of 16:06, 1 May 2009

## 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 syntax):

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

Now, given an element representing a record, we write *e(c)* for the *e* component of structure