定義域と値域

VDM++ での map 型には、写像の定義域と値域を定義できます。VDM++ では、次のように表現します。

    dom {'A' |-> 1, 'B' |-> 2, 'C' |-> 3}        = {A, B, C}

写像 {'A' |-> 1, 'B' |-> 2, 'C' |-> 3} の定義域は {A, B, C} になります。

    rng {'A' |-> 1, 'B' |-> 2, 'C' |-> 3}        = {1, 2, 3}

写像 {'A' |-> 1, 'B' |-> 2, 'C' |-> 3} の値域は {1, 2, 3} になります。
ただし、空写像にこれらの演算を利用すると、空集合が得られます。