Difference between revisions of "Structured Types"

From Event-B
Jump to navigationJump to search
imported>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):
  

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

 \begin{array}{lcl}
 \textbf{RECORD}~~~~ C &::&  e\in E\\
    &&  f \in F
 \end{array}

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

 \begin{array}{l}
 \textbf{SETS}~~ C\\
\textbf{CONSTANTS}~~ e,~ f\\
\textbf{AXIOMS}\\
~~~~\begin{array}{l}
   e \in  C \tfun E\\
   f \in  C \tfun F\\
 \end{array} 
\end{array}


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