演算 comp を実現する

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

class VDM_Map:

    def comp(m1,m2):

        """

        m1 comp m2

            ; map B to C * map A to B -> map A to C   

            ;

            ; Map composition

            ;   yields the the map that is created by composing m2 

            ;   elements with m1 elements. The resulting map is a 

            ;   map with the same domain as m2. The information 

            ;   value corresponding to a key is the one found by 

            ;   first applying m2 to the key and then applying m1 

            ;   to the result. rng m2 must be a subset of dom m1. 

        """

        assert m1._pre_Map_composition(m2)

        return VDM_Map(m1._Map_composition(m2))

    def _Map_composition(m1,m2):

        m = {}

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

            m[k] = m1.dict[v]

        return m

    def _pre_Map_composition(m1,m2):

        rs,ds = rng(m2),dom(m1)

        assert rs.subset(ds),(

            "::: %s comp %s \n"

                %(m1,m2)+

            ":::\t (>>%s<<).subset(%s) \n"

                %(rs,ds)+

            ":::\t m comp n: rng m2 must be a subset of dom m1"

            )

        return True

メソッド comp は、写像 m1 および m2 を合成した写像を生成して、これをリターン値とします。このとき、写像 m2 の値域に含まる要素をキーとして、写像 m1 から対応する値を獲得します。メソッド _Map_composition は、comp の補助関数です。まず、空の辞書 m を用意して、写像 m2 に含まれるすべての写像対 k,v に対して、m2 のキーと、それに対応する m1 の要素とを、辞書の項目として追加します。メソッド _pre_Map_composition は、事前条件を検証します。写像 m2 の値域が、写像 m1 の定義域の部分集合でないなら、エラーメッセージを表示します。