演算 ** を実現する

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

class VDM_Map:

    def __pow__(m,n):

        """

        m ** n

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

            ;

            ; Map iteration

            ;   yields the map where m is composed with itself 

            ;   n times. n=0 yields the identity map where each 

            ;   element of dom m is map into itself; n=1 yields m 

            ;   itself. For n>1, the range of m must be a subset of 

            ;   dom m. 

        """

        return VDM_Map(m._Map_iteration(n))

    def _Map_iteration(m,n):

        mm = {}

        assert m._pre_Map_iteration(n)

        mdict = m.dict

        for k,v in mdict.items():

            acc,c = k,n

            while c > 0:

                acc = mdict[acc]

                c -= 1

            mm[k] = acc

        return mm

    def _pre_Map_iteration(m,n):

        rm,dm = rng(m),dom(m)

        assert rm.subset(dm),(

            "::: %s ** %s\n"

                %(m,n)+

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

                %(rm,dm)+

            ":::\t m ** n: the range of m must be a subset of dom m"

            )

        return True

メソッド __pow__ では、演算子 ** の動作を規定します。同一写像 m を n 回繰り返して適用する写像を生成して、これをリターン値とします。メソッド _Map_iteration は、__pow__ の補助関数です。まず、空の辞書 mm を用意して、辞書 mdict に含まれるすべてのキー k と、それに対応する値を n 回繰り返して得られる値 acc とを、辞書 mm の項目として追加します。メソッド _pre_Map_iteration は、事前条件を検証します。写像 m の値域が、その定義域の部分集合でないなら、エラーメッセージを表示します。
《Note》Python の演算子 ** には、次のメソッドが対応します。
__pow__(self, other[, modulo])
演算子 ** を利用したときの処理を規定します。□