演算 <: および <-: を実現する

VDM++ での演算 <: および <-: に準拠するように、メソッド VDM_Map.domTo/VDM_Map.domBy を実現します。

class VDM_Map:

    def domTo(m,s):

        """

        s <: m
            ; set of A * map A to B -> map A to B 

            ;

            ; Domain restricted to

            ;   creates the map consisting of the elements in m 

            ;   whose key is in s. s need not be a subset of dom 

            ;   m. 

        """

        return VDM_Map(m._domain(dom(m).inter(s)))
    def domBy(m,s):

        """

        s <-: m

            ; set of A * map A to B -> map A to B 

            ;

            ; Domain restricted by 

            ;   creates the map consisting of the elements in m 

            ;   whose key is not in s. s need not be a subset of 

            ;   dom m. 

        """

        return VDM_Map(m._domain(dom(m) - s))
    def _domain(m,s):

        mm = {}

        for e in s:

            mm[e] = m.dict[e]

        return mm

メソッド domTo では、写像 m の定義域を集合 s の要素に限定した写像を生成して、これをリターン値とします。
メソッド domBy では、写像 m の定義域から集合 s の要素を削除した写像を生成して、これをリターン値とします。
メソッド _domain は、domTo/domBy に共通の補助関数です。空の辞書 mm を用意して、集合 s の要素 e だけをキーとして、写像 m の対応する値だけを追加します。