写像の併合
VDM++ の map 型には、 複数の写像をもとに新たな写像を定義できます。VDM++ では、次のように表現します。
{"A" |-> 1, "B" |-> 2} munion {"A" |-> 1, "C" |-> 3}
= {"A" |-> 1, "B" |-> 2, "C" |-> 3}２つの写像を併合した写像は {"A" |-> 1, "B" |-> 2, "C" |-> 3} になります。このとき、２つの写像には同じ写像対 "A" |-> 1 が含まれます。
{"A" |-> 1, "B" |-> 2} ++ {"A" |-> 0, "C" |-> 3}
= {"A" |-> 0, "B" |-> 2, "C" |-> 3}一方の写像に他方の写像を上書きした写像は {"A" |-> 0, "B" |-> 2, "C" |-> 3} になります。このとき、２つの写像には同じキー "A" が含まれますが、写像対 "A" |-> 0 を上書きします。
merge {{'A' |-> 1, 'C' |-> 3}, {'A' |-> 1, 'B' |-> 2}}
= {"A" |-> 1, "B" |-> 2, "C" |-> 3}
（集合の要素として列挙された）すべての写像を併合した写像は {"A" |-> 1, "B" |-> 2, "C" |-> 3} になります。このとき、これらの写像には同じ写像対 "A" |-> 1 が含まれます。
事例：演算 munion
VDM++ での演算 munion に準拠した事例（VDM_Map.munion）を紹介します。
m1 = VDM_Map({"A":1,"B":2})
m2 = VDM_Map({"A":1,"C":3})
print ">>> %s munion %s"%(m1,m2)
X = m1.munion(m2)
print X; assert X == VDM_Map({"A":1,"B":2,"C":3})
写像 m1 および m2 を併合した写像を得るには、メソッド munion を利用します。このコードを実行すると、
>>> {'A' |-> 1, 'B' |-> 2} munion {'A' |-> 1, 'C' |-> 3}
{'A' |-> 1, 'C' |-> 3, 'B' |-> 2}併合した写像は {'A' |-> 1, 'C' |-> 3, 'B' |-> 2} になります。このとき、写像対の順序には、意味がありません。
m1 = VDM_Map({"A":1,"B":2})
m2 = VDM_Map({"A":0,"C":3})
print ">>> %s munion %s"%(m1,m2)
try:
X = m1.munion(m2)
except AssertionError,name:
print name
写像 m1 および m2 において、同じキーに異なる値が対応するなら、この演算を利用できません。このコードを実行すると、
>>> {'A' |-> 1, 'B' |-> 2} munion {'A' |-> 0, 'C' |-> 3}
- : {'A' |-> 1, 'B' |-> 2} munion {'A' |-> 0, 'C' |-> 3}
- : A |-> (>>1<<) == A |-> (>>0<<)
例外を生成して、エラーメッセージが表示されます。なぜなら、同じキー A に対して、異なる値 1 および 0 が対応するからです。
演算 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 が得られます。□
事例：演算 ++
VDM++ での演算 ++ に準拠した事例（演算子 +）を紹介します。
m1 = VDM_Map({"A":1,"B":2})
m2 = VDM_Map({"A":1,"C":3})
print ">>> %s ++ %s"%(m1,m2)
X = m1 + m2
print X; assert X == VDM_Map({"A":1,"B":2,"C":3})
写像 m1 に m2 を上書きした写像を得るには、演算子 + を利用します。このコードを実行すると、
>>> {'A' |-> 1, 'B' |-> 2} ++ {'A' |-> 1, 'C' |-> 3}
{'A' |-> 1, 'C' |-> 3, 'B' |-> 2}上書きした写像は {'A' |-> 1, 'C' |-> 3, 'B' |-> 2} になります。このとき、写像対の順序には、意味がありません。
m1 = VDM_Map({"A":1,"B":2})
m2 = VDM_Map({"A":0,"C":3})
print ">>> %s ++ %s"%(m1,m2)
X = m1 + m2
print X; assert X == VDM_Map({"A":0,"B":2,"C":3})
写像 m1 および m2 において、同じキーに異なる値が対応すると、これを上書きします。このコードを実行すると、
>>> {'A' |-> 1, 'B' |-> 2} ++ {'A' |-> 0, 'C' |-> 3}
{'A' |-> 0, 'C' |-> 3, 'B' |-> 2}上書きした写像は {'A' |-> 0, 'C' |-> 3, 'B' |-> 2} になります。このとき、同じキー A に対して、上書きした値 0 が対応しています。
演算 ++ を実現する
VDM++ での演算 ++ に準拠するように、メソッド VDM_Map.__add__ を実現します。
class VDM_Map:
def __add__(m1,m2):
"""
m1 ++ m2
; map A to B * map A to B -> map A to B
;
; Override
; overrides and merges m1 with m2, i.e. it is like a
; merge except that m1 and m2 need not be compat-
; ible; any common elements are mapped as by m2
; (so m2 overrides m1).
"""
return VDM_Map(m1._Override(m2))
def _Override(m1,m2):
m = {}
for k,v in m1.dict.items():
m[k] = v
for k,v in m2.dict.items():
m[k] = v
return m
メソッド __add__ では、演算子 + の動作を規定します。写像 m1 に m2 を上書きした写像を生成して、これをリターン値とします。メソッド _Override は、munion の補助関数です。まず、空の辞書 m を用意して、写像 m1 に含まれるすべての写像対を追加します。次に、写像 m2 に含まれるすべての写像対を追加します。
《Note》Python の演算子 + には、次のメソッドが対応します。
__add__(self, other)
２項演算子 + を適用したときの動作を規定します。□
事例：演算 merge
VDM++ での演算 merge に準拠した事例を紹介します。
m1 = VDM_Map({"A":1,"B":2})
m2 = VDM_Map({"A":1,"C":3})
ms = VDM_Set((m1,m2) )
print ">>> merge %s"%ms
X = merge(ms)
print X; assert X == VDM_Map({"A":1,"B":2,"C":3})
（集合 ms の要素として列挙された）写像 m1 および m2 から、すべての写像を併合した写像を得るには、関数 merge を利用します。このコードを実行すると、
>>> merge {{'A' |-> 1, 'C' |-> 3}, {'A' |-> 1, 'B' |-> 2}}
{'A' |-> 1, 'C' |-> 3, 'B' |-> 2}併合した写像は {'A' |-> 1, 'C' |-> 3, 'B' |-> 2} になります。このとき、写像対の順序には、意味がありません。
m1 = VDM_Map({"A":1,"B":2})
m2 = VDM_Map({"A":0,"C":3})
ms = VDM_Set((m1,m2) )
print ">>> merge %s"%ms
try:
X = merge(ms)
except AssertionError,name:
print name
（集合 ms の要素として列挙された）写像 m1 および m2 において、同じキーに異なる値が対応するなら、この演算を利用できません。このコードを実行すると、
>>> merge {{'A' |-> 0, 'C' |-> 3}, {'A' |-> 1, 'B' |-> 2}}
- : {'A' |-> 0, 'C' |-> 3} munion {'A' |-> 1, 'B' |-> 2}
- : A |-> (>>0<<) == A |-> (>>1<<)
例外を生成して、エラーメッセージが表示されます。なぜなら、同じキー A に対して、異なる値 1 および 0 が対応するからです。
演算 merge を実現する
VDM++ での演算 merge に準拠するように（モジュール VDM_Map で）関数 merge を実現します。
def merge(set1):
"""
merge ms
; set of (map A to B) -> map A to B
;
; Distributed merge
; yields the map that is constructed by merging all
; the maps in ms. The maps in ms must be compat-
; ible.
"""
m = VDM_Map()
for e in ms.list:
m = m.munion(e)
return m
関数 merge では（集合 ms の要素として列挙された）すべての写像を併合した写像を生成して、これをリターン値とします。新たな写像 m を用意して、集合 ms に含まれるすべての写像 e を併合します。このとき、他で作成したメソッド munion を再利用しています。
《ひよ子のきもち♪2006/10/24》
