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