定義域と値域の限定

VDM++ の map 型には、定義域および値域を限定/削除した、新たな写像を定義できます。VDM++ では、次のように表現します。

    {'A', 'C'} <: {'A' |-> 1, 'B' |-> 2}    = {'A' |-> 1}

写像 {'A' |-> 1, 'B' |-> 2} の定義域を、キー集合 {'A', 'C'} の要素に限定すると {'A' |-> 1} になります。このとき、要素 'C' は写像の定義域に含まれないので、無視されます。

    {'A', 'C'} <-: {'A' |-> 1, 'B' |-> 2}    = {'B' |-> 2}

写像 {'A' |-> 1, 'B' |-> 2} の定義域から、キー集合 {'A', 'C'} の要素を削除すると {'B' |-> 2} になります。このとき、要素 'C' は写像の定義域に含まれないので、無視されます。

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

写像 {'A' |-> 1, 'B' |-> 2} の値域を、値集合 {1, 3} の要素に限定すると {'A' |-> 1} になります。このとき、要素 3 は写像の値域に含まれないので、無視されます。

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

写像 {'A' |-> 1, 'B' |-> 2} の値域から、値集合 {1, 3} の要素を削除すると {'B' |-> 2} になります。このとき、要素 3 は写像の値域に含まれないので、無視されます。