写像の適用

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

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

この写像にキー 'C' を適用した値は 3 になります。ただし、指定したキーは、定義域に含まれるものとします。

    {1 |-> "alpha", 2 |-> "beta"} comp {'A' |-> 1, 'B' |-> 2}

    = {'A' |-> "alpha", 'B' |-> "beta"}

２つの写像を合成した写像は {'A' |-> "alpha", 'B' |-> "beta"} になります。ただし、一方の写像の値域が、他方の写像の定義域の部分集合になるものとします。

    {4 |-> 1, 3 |-> 4, 2 |-> 3, 1 |-> 2} ** 2

    = {4 |-> 2, 3 |-> 1, 2 |-> 4, 1 |-> 3}

同一写像を繰り返し適用した写像は {4 |-> 2, 3 |-> 1, 2 |-> 4, 1 |-> 3} になります。ただし、同一写像の値域が、同一写像の定義域の部分集合になるものとします。