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 ''R'' 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):
 
Let us use the following syntax for this (not part of Event-B syntax):
  
Line 9: Line 9:
 
{{SimpleHeader}}
 
{{SimpleHeader}}
 
|<math> \begin{array}{lcl}
 
|<math> \begin{array}{lcl}
  \textbf{RECORD}~~~~ C &::&  e\in E\\
+
  \textbf{RECORD}~~~~ R &::&  e\in E\\
 
     &&  f \in F
 
     &&  f \in F
 
  \end{array}  
 
  \end{array}  
Line 16: Line 16:
 
</center>
 
</center>
  
We can model this structure in Event-B by introducing (in a context) a carrier set ''C'' and two
+
We can model this structure in Event-B by introducing (in a context) a carrier set ''R'' and two
 
functions ''e'' and ''f'' as constants as follows:
 
functions ''e'' and ''f'' as constants as follows:
  
Line 22: Line 22:
 
{{SimpleHeader}}
 
{{SimpleHeader}}
 
|<math> \begin{array}{l}
 
|<math> \begin{array}{l}
  \textbf{SETS}~~ C\\
+
  \textbf{SETS}~~ R\\
 
\textbf{CONSTANTS}~~ e,~ f\\
 
\textbf{CONSTANTS}~~ e,~ f\\
 
\textbf{AXIOMS}\\
 
\textbf{AXIOMS}\\
 
~~~~\begin{array}{l}
 
~~~~\begin{array}{l}
   e \in  C \tfun E\\
+
   e \in  R \tfun E\\
   f \in  C \tfun F\\
+
   f \in  R \tfun F\\
 
  \end{array}  
 
  \end{array}  
 
\end{array}  
 
\end{array}  
Line 35: Line 35:
  
  
Now, given an element <math>c\in C</math> representing a record structure, we write <math>e(c)</math> for the ''e'' component of ''c'' and <math>f(c)</math> for the ''f'' component of ''c''.
+
Now, given an element <math>r\in R</math> representing a record structure, we write <math>e(r)</math> for the ''e'' component of ''r'' and <math>f(r)</math> for the ''f'' component of ''r''.
  
 
''E'' and ''F'' can be any  type definable in Event-B, including a type representing a record structure.
 
''E'' and ''F'' can be any  type definable in Event-B, including a type representing a record structure.
Line 41: Line 41:
 
==Constructing Structured Values==
 
==Constructing Structured Values==
  
Suppose we have a variable ''v'' in a machine whose type is the structure ''C'' defined above:
+
Suppose we have a variable ''v'' in a machine whose type is the structure ''R'' defined above:
 
<center>
 
<center>
<math>\textit{VARIABLE}~~ v\in C</math>
+
<math>\textbf{VARIABLE}~~ v\in R</math>
 
</center>
 
</center>
 
We wish to assign a structured value to ''v'' whose ''e'' field has some value ''e1'' and whose ''f'' field has some value ''f1''.
 
We wish to assign a structured value to ''v'' whose ''e'' field has some value ''e1'' and whose ''f'' field has some value ''f1''.
This can be achieved by specifying the choice of an event parameter ''c'' whose fields are constrained by appropriate guards
+
This can be achieved by specifying the choice of an event parameter ''r'' whose fields are constrained by appropriate guards
and assigning parameter ''c'' to the machine variable ''v''.  This is shown in the following event:
+
and assigning parameter ''r'' to the machine variable ''v''.  This is shown in the following event:
  
 
<center><math>
 
<center><math>
 
\begin{array}{l}  
 
\begin{array}{l}  
\textit{ANY}~~ c ~~\textit{WHERE} \\  
+
\textbf{ANY}~~ r ~~\textbf{WHERE} \\  
~~~~ c \in C \\
+
~~~~ r \in R \\
~~~~ e( c ) = e1 \\
+
~~~~ e( r ) = e1 \\
~~~~ f( c ) = f1 \\  
+
~~~~ f( r ) = f1 \\  
\textit{THEN} \\
+
\textbf{THEN} \\
~~~~ v := c \\
+
~~~~ v := r \\
\textit{END}
+
\textbf{END}
 
\end{array}
 
\end{array}
 
</math></center>
 
</math></center>
Line 66: Line 66:
 
<center><math>
 
<center><math>
 
\begin{array}{l}  
 
\begin{array}{l}  
\textit{ANY}~~ c ~~\textit{WHERE} \\  
+
\textbf{ANY}~~ r ~~\textbf{WHERE} \\  
~~~~ c \in C \\
+
~~~~ r \in R \\
~~~~ e( c ) = e1 \\
+
~~~~ e( r ) = e1 \\
~~~~ f( c ) = f(v) \\  
+
~~~~ f( r ) = f(v) \\  
\textit{THEN} \\
+
\textbf{THEN} \\
~~~~ v := c \\
+
~~~~ v := r \\
\textit{END}
+
\textbf{END}
 
\end{array}
 
\end{array}
 
</math></center>
 
</math></center>
Line 80: Line 80:
 
<center><math>
 
<center><math>
 
\begin{array}{l}  
 
\begin{array}{l}  
\textit{ANY}~~ c ~~\textit{WHERE} \\  
+
\textbf{ANY}~~ r ~~\textbf{WHERE} \\  
~~~~ c \in C \\
+
~~~~ r \in R \\
~~~~ e( c ) = e1 \\
+
~~~~ e( r ) = e1 \\
\textit{THEN} \\
+
\textbf{THEN} \\
~~~~ v := c \\
+
~~~~ v := r \\
\textit{END}
+
\textbf{END}
 
\end{array}
 
\end{array}
 
</math></center>
 
</math></center>
Line 92: Line 92:
 
Sometimes we will wish to model a set of structured elements as a machine variable, e.g.,
 
Sometimes we will wish to model a set of structured elements as a machine variable, e.g.,
 
<center>
 
<center>
<math>\textit{VARIABLE}~~ vs\subseteq C</math>
+
<math>\textbf{VARIABLE}~~ vs\subseteq R</math>
 
</center>
 
</center>
  
Line 98: Line 98:
 
<center><math>
 
<center><math>
 
\begin{array}{l}  
 
\begin{array}{l}  
\textit{ANY}~~ c ~~\textit{WHERE} \\  
+
\textbf{ANY}~~ r ~~\textbf{WHERE} \\  
~~~~ c \in C \\
+
~~~~ r \in R \\
~~~~ e( c ) = e1 \\
+
~~~~ e( r ) = e1 \\
~~~~ f( c ) = f1 \\  
+
~~~~ f( r ) = f1 \\  
\textit{THEN} \\
+
\textbf{THEN} \\
~~~~ vs := vs \cup \{c\} \\
+
~~~~ vs := vs \cup \{r\} \\
\textit{END}
+
\textbf{END}
 
\end{array}
 
\end{array}
 
</math></center>
 
</math></center>

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

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

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

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


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

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

Constructing Structured Values

Suppose we have a variable v in a machine whose type is the structure R defined above:

\textbf{VARIABLE}~~ v\in R

We wish to assign a structured value to v whose e field has some value e1 and whose f field has some value f1. This can be achieved by specifying the choice of an event parameter r whose fields are constrained by appropriate guards and assigning parameter r to the machine variable v. This is shown in the following event:


\begin{array}{l} 
\textbf{ANY}~~ r ~~\textbf{WHERE} \\ 
~~~~ r \in R  \\
~~~~ e( r ) = e1 \\
~~~~ f( r ) = f1 \\ 
\textbf{THEN} \\
~~~~ v := r \\
\textbf{END}
\end{array}

If we only wish to update some fields and leave others changed, this needs to be done by specifying explicitly that some fields remain unchanged. This is shown in the following example where only the e field is modified:


\begin{array}{l} 
\textbf{ANY}~~ r ~~\textbf{WHERE} \\ 
~~~~ r \in R  \\
~~~~ e( r ) = e1 \\
~~~~ f( r ) = f(v) \\ 
\textbf{THEN} \\
~~~~ v := r \\
\textbf{END}
\end{array}

If we don't care about the value of some field (e.g., f), we simply omit any guard on that field as follows:


\begin{array}{l} 
\textbf{ANY}~~ r ~~\textbf{WHERE} \\ 
~~~~ r \in R  \\
~~~~ e( r ) = e1 \\
\textbf{THEN} \\
~~~~ v := r \\
\textbf{END}
\end{array}


Sometimes we will wish to model a set of structured elements as a machine variable, e.g.,

\textbf{VARIABLE}~~ vs\subseteq R

We can add a structured element to this set using the following event:


\begin{array}{l} 
\textbf{ANY}~~ r ~~\textbf{WHERE} \\ 
~~~~ r \in R  \\
~~~~ e( r ) = e1 \\
~~~~ f( r ) = f1 \\ 
\textbf{THEN} \\
~~~~ vs := vs \cup \{r\} \\
\textbf{END}
\end{array}

Extending Structured Types

Sub-Typing

Recursive Structured Types

Structured Variables