定義域と値域の限定
VDM++ の map 型には、定義域および値域を限定/削除した、新たな写像を定義できます。VDM++ では、次のように表現します。
{'A', 'C'} <: {'A' |-> 1, 'B' |-> 2} = {'A' |-> 1}写像 {'A' |-> 1, 'B' |-> 2} の定義域を、キー集合 {'A', 'C'} の要素に限定すると {'A' |-> 1} になります。このとき、要素 'C' は写像の定義域に含まれないので、無視されます。
{'A', 'C'} <-: {'A' |-> 1, 'B' |-> 2} = {'B' |-> 2}写像 {'A' |-> 1, 'B' |-> 2} の定義域から、キー集合 {'A', 'C'} の要素を削除すると {'B' |-> 2} になります。このとき、要素 'C' は写像の定義域に含まれないので、無視されます。
{'A' |-> 1, 'B' |-> 2} :> {1, 3} = {'A' |-> 1}写像 {'A' |-> 1, 'B' |-> 2} の値域を、値集合 {1, 3} の要素に限定すると {'A' |-> 1} になります。このとき、要素 3 は写像の値域に含まれないので、無視されます。
{'A' |-> 1, 'B' |-> 2} :-> {1, 3} = {'B' |-> 2}写像 {'A' |-> 1, 'B' |-> 2} の値域から、値集合 {1, 3} の要素を削除すると {'B' |-> 2} になります。このとき、要素 3 は写像の値域に含まれないので、無視されます。
演算 <: および <-: を実現する
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 の対応する値だけを追加します。
演算 :> および :-> を実現する
VDM++ での演算 :> および :-> に準拠するように、メソッド VDM_Map.rngTo/VDM_Map.rngBy を実現します。
class VDM_Map:
def rngTo(m,s):
"""
m :> s
; map A to B * set of B -> map A to B
;
; Range restricted to
; creates the map consisting of the elements in m
; whose information value is in s. s need not be a
; subset of rng m.
"""
return VDM_Map(m._range(rng(m).inter(s)))def rngBy(m,s):
"""
m :-> s
; map A to B * set of B -> map A to B
;
; Range restricted by
; creates the map consisting of the elements in m
; whose information value is not in s. s need not be
; a subset of rng m.
"""
return VDM_Map(m._range(rng(m) - s))def _range(m,s):
mm = {}
for k,v in m.dict.items():
if v in s:
mm[k] = v
return mm
メソッド rngTo では、写像 m の値域を集合 s の要素に限定した写像を生成して、これをリターン値とします。
メソッド rngBy では、写像 m の値域から集合 s の要素を削除した写像を生成して、これをリターン値とします。
メソッド _range は、rngTo/rngBy に共通の補助関数です。空の辞書 mm を用意して、写像 m のすべての写像対 k,v について、集合 s の要素 v だけを値として追加します。
《ひよ子のきもち♪2006/10/25》
事例：演算 <:
VDM++ での演算 <: に準拠した事例（VDM_Map.domTo）を紹介します。
m = VDM_Map({"A":1,"B":2})
s = VDM_Set(["A","C"])
print ">>> %s <: %s"%(s,m) X = m.domTo(s)
print X; assert X == VDM_Map({"A":1})
写像 m の定義域を集合 s の要素に限定した写像を得るには、メソッド domTo を利用します。このコードを実行すると、
>>> {'A', 'C'} <: {'A' |-> 1, 'B' |-> 2}
{'A' |-> 1}定義域を限定した写像は {'A' |-> 1} になります。
事例：演算 :>
VDM++ での演算 :> に準拠した事例（VDM_Map.rngTo）を紹介します。
m = VDM_Map({"A":1,"B":2})
s = VDM_Set([1,3])
print ">>> %s :> %s"%(s,m)
X = m.rngTo(s)
print X; assert X == VDM_Map({"A":1})
写像 m の値域を集合 s の要素に限定した写像を得るには、メソッド rngTo を利用します。このコードを実行すると、
>>> {1, 3} :> {'A' |-> 1, 'B' |-> 2}
{'A' |-> 1}値域を限定した写像は {'A' |-> 1} になります。
事例：演算 :->
VDM++ での演算 :-> に準拠した事例（VDM_Map.rngBy）を紹介します。
m = VDM_Map({"A":1,"B":2})
s = VDM_Set([1,3])
print ">>> %s :-> %s"%(m,s)
X = m.rngBy(s)
print X; assert X == VDM_Map({"B":2})
写像 m の値域から集合 s の要素を削除した写像を得るには、メソッド rngBy を利用します。このコードを実行すると、
>>> {'A' |-> 1, 'B' |-> 2} :-> {1, 3}
{'B' |-> 2}値域から削除した写像は {'B' |-> 2} になります。
事例：演算 <-:
VDM++ での演算 <-: に準拠した事例（VDM_Map.domBy）を紹介します。
m = VDM_Map({"A":1,"B":2})
s = VDM_Set(["A","C"])
print ">>> %s <-: %s"%(s,m)
X = m.domBy(s)
print X; assert X == VDM_Map({"B":2})
写像 m の定義域から集合 s の要素を削除した写像を得るには、メソッド domBy を利用します。このコードを実行すると、
>>> {'A', 'C'} <-: {'A' |-> 1, 'B' |-> 2}
{'B' |-> 2}定義域から削除した写像は {'B' |-> 2} になります。
