定義域と値域の限定
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 は写像の値域に含まれないので、無視されます。