Editing Vienna Development Method (section)

===Collections===
Collection types model groups of values. Sets are finite unordered collections in which duplication between values is suppressed. Sequences are finite ordered collections (lists) in which duplication may occur and mappings represent finite correspondences between two sets of values.

==== Sets ====
The set type constructor (written <code>set of T</code> where <code>T</code> is a predefined type) constructs the type composed of all finite sets of values drawn from the type <code>T</code>. For example, the type definition
<syntaxhighlight lang="rsl">
UGroup = set of UserId
</syntaxhighlight>
defines a type <code>UGroup</code> composed of all finite sets of <code>UserId</code> values. Various operators are defined on sets for constructing their union, intersections, determining proper and non-strict subset relationships etc.

{| border="1" class="wikitable"
|+ style="background:#ffdead;" |Main operators on sets (s, s1, s2 are sets)
|-
| <code>{a, b, c}</code> || Set enumeration: the set of elements <code>a</code>, <code>b</code> and <code>c</code>
|-
| <code><nowiki>{x | x:T & P(x)}</nowiki></code> || Set comprehension: the set of <code>x</code> from type <code>T</code> such that <code>P(x)</code>
|-
| <code>{i, ..., j}</code> || The set of integers in the range <code>i</code> to <code>j</code>
|-
| <code>e in set s</code> || <code>e</code> is an element of set <code>s</code>
|-
| <code>e not in set s</code> || <code>e</code> is not an element of set <code>s</code>
|-
| <code>s1 union s2</code> || Union of sets <code>s1</code> and <code>s2</code>
|-
| <code>s1 inter s2</code> || Intersection of sets <code>s1</code> and <code>s2</code>
|-
| <code>s1 \ s2</code> || Set difference of sets <code>s1</code> and <code>s2</code>
|-
| <code>dunion s</code> || Distributed union of set of sets <code>s</code>
|-
| <code>s1 psubset s2</code> || s1 is a (proper) subset of <code>s2</code>
|-
| <code>s1 subset s2</code>  || s1 is a (weak) subset of <code>s2</code>
|-
| <code>card s</code> || The cardinality of set <code>s</code>
|}

==== Sequences ====
The finite sequence type constructor (written <code>seq of T</code> where <code>T</code> is a predefined type) constructs the type composed of all finite lists of values drawn from the type <code>T</code>. For example, the type definition
<syntaxhighlight lang="rsl">
String = seq of char
</syntaxhighlight>
Defines a type <code>String</code> composed of all finite strings of characters. Various operators are defined on sequences for constructing concatenation, selection of elements and subsequences etc. Many of these operators are partial in the sense that they are not defined for certain applications. For example, selecting the 5th element of a sequence that contains only three elements is undefined.

The order and repetition of items in a sequence is significant, so <code>[a, b]</code> is not equal to  <code>[b, a]</code>, and <code>[a]</code> is not equal to <code>[a, a]</code>.

{| border="1" class="wikitable"
|+ style="background:#ffdead;" |Main operators on sequences (s, s1,s2 are sequences)
|-
| <code>[a, b, c]</code> || Sequence enumeration: the sequence of elements <code>a</code>, <code>b</code> and <code>c</code>
|-
| <code><nowiki>[f(x) | x:T & P(x)]</nowiki></code> || Sequence comprehension: sequence of expressions <code>f(x)</code> for each <code>x</code> of (numeric) type <code>T</code> such that <code>P(x)</code> holds <br />(<code>x</code> values taken in numeric order)
|-
| <code>hd s</code> || The head (first element) of <code>s</code>
|-
| <code>tl s</code> || The tail (remaining sequence after head is removed) of <code>s</code>
|-
| <code>len s</code> || The length of <code>s</code>
|-
| <code>elems s</code> || The set of elements of <code>s</code>
|-
| <code>s(i)</code> || The <code>i</code><sup>th</sup> element of <code>s</code>
|-
| <code>inds s</code> || the set of indices for the sequence <code>s</code>
|-
| <code>s1^s2</code> || the sequence formed by concatenating sequences <code>s1</code> and <code>s2</code>
|}

==== 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>
|}