演算 munion を実現する

VDM++ での演算 munion に準拠するように、メソッド VDM_Map.munion を実現します。

class VDM_Map:

    def munion(m1,m2):

        """

        m1 munion m2

            ; (map A to B) * (map A to B) -> map A to B

            ;

            ; Merge

            ;   yields a map combined by m1 and m2 such that 

            ;   the resulting map maps the elements of dom m1 as 

            ;   does m1, and the elements of dom m2 as does m2. 

            ;   The two maps must be compatible.

        """

        return VDM_Map(m1._Merge(m2))

    def _Merge(m1,m2):

        m = {}

        for k,v in m1.dict.items():

            m[k] = v

        for k,v in m2.dict.items():

            if m.has_key(k):

                assert m1._pre_Merge_(m2,m,k,v)

            m[k] = v

        return m

    def _pre_Merge_(m1,m2,m,k,v):

        assert m[k] == v,(

            "::: %s munion %s\n"

                %(m1,m2)+

            ":::\t%s |-> (>>%s<<) == %s |-> (>>%s<<)"

                %(k,m[k],k,v)

            )

        return True

メソッド munion では、写像 m1 および m2 を併合した写像を生成して、これをリターン値とします。
メソッド _Merge は、munion の補助関数です。まず、空の辞書 m を用意して、写像 m1 に含まれるすべての写像対を追加します。次に、写像 m2 に含まれるすべての写像対の中から、m とキーが重複しないものだけを追加します。
メソッド _pre_Merge_ は、事前条件を検証します。写像 m1 と m2 とで写像対が一致しないなら、エラーメッセージを表示します。これによって、２つの写像対が一致することを保証します。

《Note》Python の組み込み型 dict には、次のメソッドが規定されています。
a.items()
変数 a が dict 型の値を束縛するとき、その写像対をすべてコピーした、list 型の値が得られます。
a.has_key(k)
変数 a が dict 型の値を束縛するとき、任意の型の値 k をキーとするなら True が、それ以外は False が得られます。□