演算 () を実現する

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

class VDM_Map:

    def __getitem__(m,d):

        """

        m(d)

            ; map A to B * A -> B 

            ;

            ; Map apply

            ;   yields the information value whose key is d. d must 

            ;   be in the domain of m. 

        """

        assert m._pre_Map_apply_(d)

        return m.dict[d]

    def _pre_Map_apply_(m,d):

        dm = dom(m)

        assert d in dm,(

            "::: %s(%s)\n"

                %(m,d)+

            ":::\t (>>%s<<) in %s \n"

                %(d,dm)+

            ":::\t m(d): d must be in the domain of m"

            )

        return True

メソッド __getitem__ では、演算子 の動作を規定します。辞書 m.dict のキー d に対応する値を獲得して、これをリターン値とします。メソッド _pre_Map_apply_ は、事前条件を検証します。指定したキー d が、写像 m の定義域に含まれないなら、エラーメッセージを表示します。

《Note》Python の演算子 には、次のメソッドが対応します。
__getitem__(self, key)
演算子 [] を利用したときの動作を規定します。□