Download as a PDF

where is-disj means that the two given sets are disjunct i.e. they have no common elements.
An example for a partition can be seen below. The given set consists of two
sets which are disjunct.
{pa , pb } ⊆ P artition
pa = {{1}, {2}}}
pb = {{1, 2}}
3.4
Composite Objects
Sets are not the only data structures used in VDM. Another kind of collections
are multicomponent objects, so called composite objects. Composite objects can
be compared with structures in C or records in Pascal. Such an object consists
of various fields, each having a (different) value.
3.4.1
Defining Composite Objects
While classes of sets are defined by the -set constructor, composite objects are
defined in another way:
compose [objectname] of
[f ieldname] : [f ieldtype],
...
end
The objectname defines a name for the composite object. A composite object
can consist of different fields whose name and type are set in the definition and
separated by commas. An example for a composite object is a Date-Object
which consists of two values, the day and the year.
compose Datec of
day : {1, ..., 366},
year : N
end
It is not necessary to give a fieldname if the field is never accessed via its name.
The definition for a Celcius-Object containing the temperature, may be changed
17