# Difference between revisions of "Structured Types"

From Event-B

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

Line 2: | Line 2: | ||

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 | + | 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): | ||

Line 9: | Line 9: | ||

{{SimpleHeader}} | {{SimpleHeader}} | ||

|<math> \begin{array}{lcl} | |<math> \begin{array}{lcl} | ||

− | \textbf{ | + | \textbf{RECORD}~~~~ C &::& e\in E\\ |

&& f \in F | && f \in F | ||

\end{array} | \end{array} | ||

Line 35: | Line 35: | ||

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

− | |||

− | |||

− | |||

− | |||

− | |||

− | |||

− | |||

− | |||

− | |||

− | |||

− | '' | ||

− | |||

− |

## Revision as of 16:03, 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):

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