Editing Vienna Development Method (section)

==== Maps ====
A finite mapping is a correspondence between two sets, the domain and range, with the domain indexing elements of the range. It is therefore similar to a finite function. The mapping type constructor in VDM-SL (written <code>map T1 to T2</code> where <code>T1</code> and <code>T2</code> are predefined types) constructs the type composed of all finite mappings from sets of <code>T1</code> values to sets of <code>T2</code> values. For example, the type definition
<syntaxhighlight lang="rsl">
Birthdays = map String to Date
</syntaxhighlight>
Defines a type <code>Birthdays</code> which maps character strings to <code>Date</code>. Again, operators are defined on mappings for indexing into the mapping, merging mappings, overwriting extracting sub-mappings.

{| border="1" class="wikitable"
|+ style="background:#ffdead;" |Main operators on mappings
|-
| <code><nowiki>{a |-> r, b |-> s}</nowiki></code> || Mapping enumeration: <code>a</code> maps to <code>r</code>, <code>b</code> maps to <code>s</code>
|-
| <code><nowiki>{x |-> f(x) | x:T & P(x)}</nowiki></code> || Mapping comprehension: <code>x</code> maps to <code>f(x)</code> for all <code>x</code> for type <code>T</code> such that <code>P(x)</code>
|-
| <code>dom m</code> || The domain of <code>m</code>
|-
| <code>rng m</code> || The range of <code>m</code>
|-
| <code>m(x)</code> || <code>m</code> applied to <code>x</code>
|-
| <code>m1 munion m2</code> || Union of mappings <code>m1</code> and <code>m2</code> (<code>m1</code>, <code>m2</code> must be consistent where they overlap)
|-
| <code>m1 ++ m2</code> || <code>m1</code> overwritten by <code>m2</code>
|}