Design and Analysis of Algorithms

Formal Specifi cations—1 Model Oriented 573

of the composite type) and creates a value of the type. The letters mk- are placed with the component type

name and followed by the component values in brackets. Here are some examples of values of the composite

type Co_ordinate:

mk-Co_ordinate(0, 0, 0)

mk-Co_ordinate(1, 2, 3)

mk-Co_ordinate(11, 42, 333)

The ‘mk’ operator constructs composites, but we also need to access or select their individual components.

In VDM, component names are used as selector functions, returning the value in their slot. These selectors

can be in written with a prefi x function syntax, or after a dot extension. Thus we can write:

xaxis( mk-Co_ordinate(1, 2, 3))

zaxis( mk-Co_ordinate(11, 42, 333))

yaxis( mk-Co_ordinate(1, 2, 3)) ...