Structured Types

From Event-B
Revision as of 16:11, 1 May 2009 by imported>WikiSysop (→‎Modelling Structured Types)
Jump to navigationJump to search

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

 \textbf{RECORD}~~~~ C &::&  e\in E\\
    &&  f \in F

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:

 \textbf{SETS}~~ C\\
\textbf{CONSTANTS}~~ e,~ f\\
   e \in  C \tfun E\\
   f \in  C \tfun F\\

Now, given an element c\in C representing a record structure, we write e(c) for the e component of c and f(c) for the f component of c.

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

Constructing Structured Values

Extending Structured Types

Recursive Structured Types

Structured Variables