写像の併合

VDM++ の map 型には、 複数の写像をもとに新たな写像を定義できます。VDM++ では、次のように表現します。

    {"A" |-> 1, "B" |-> 2} munion {"A" |-> 1, "C" |-> 3}

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

２つの写像を併合した写像は {"A" |-> 1, "B" |-> 2, "C" |-> 3} になります。このとき、２つの写像には同じ写像対 "A" |-> 1 が含まれます。

    {"A" |-> 1, "B" |-> 2} ++ {"A" |-> 0, "C" |-> 3}

    = {"A" |-> 0, "B" |-> 2, "C" |-> 3}

一方の写像に他方の写像を上書きした写像は {"A" |-> 0, "B" |-> 2, "C" |-> 3} になります。このとき、２つの写像には同じキー "A" が含まれますが、写像対 "A" |-> 0 を上書きします。

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

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

（集合の要素として列挙された）すべての写像を併合した写像は {"A" |-> 1, "B" |-> 2, "C" |-> 3} になります。このとき、これらの写像には同じ写像対 "A" |-> 1 が含まれます。