定義域と値域
VDM++ での map 型には、写像の定義域と値域を定義できます。VDM++ では、次のように表現します。
dom {'A' |-> 1, 'B' |-> 2, 'C' |-> 3} = {A, B, C}写像 {'A' |-> 1, 'B' |-> 2, 'C' |-> 3} の定義域は {A, B, C} になります。
rng {'A' |-> 1, 'B' |-> 2, 'C' |-> 3} = {1, 2, 3}写像 {'A' |-> 1, 'B' |-> 2, 'C' |-> 3} の値域は {1, 2, 3} になります。
ただし、空写像にこれらの演算を利用すると、空集合が得られます。
事例：演算 dom
VDM++ での演算 dom に準拠した事例を紹介します。
m = VDM_Map({"A":1,"B":2,"C":3})
print ">>> dom %s"%(m)
X = dom(m)
print X; assert X == VDM_Set("ABC")
写像 m の定義域を得るには、関数 dom を利用します。このコードを実行すると、
>>> dom {'A' |-> 1, 'C' |-> 3, 'B' |-> 2}
{'A', 'B', 'C'}定義域は {A, B, C} になります。
m = VDM_Map({})
print ">>> dom %s"%(m)
X = dom(m)
print X; assert X == VDM_Set()
空写像についても同様です。このコードを実行すると、
>>> dom {|->}
{}定義域は、空集合 {} になります。
事例：演算 rng
VDM++ での演算 rng に準拠した事例を紹介します。
m = VDM_Map({"A":1,"B":2,"C":3})
print ">>> rng %s"%(m)
X = rng(m)
print X; assert X == VDM_Set(range(1,4))
写像 m の値域を得るには、関数 rng を利用します。このコードを実行すると、
>>> rng {'A' |-> 1, 'C' |-> 3, 'B' |-> 2}
{1, 2, 3}値域は {1, 2, 3} になります。
m = VDM_Map()
print ">>> rng %s"%(m)
X = rng(m)
print X; assert X == VDM_Set()
空写像についても同様です。このコードを実行すると、
>>> rng {|->}
{}値域は、空集合 {} になります。
演算 dom/rng を実現する
VDM++ での演算 dom/rng に準拠するように（モジュール VDM_Map で）関数 dom/rng を実現します。
def dom(m):
"""
dom m
; map A to B -> set of A
;
; Domain
; yields the domain (the set of keys) of m.
"""
return VDM_Set(m.dict.keys())
関数 dom は、写像 m のキー集合を生成して、これをリターン値とします。
《関連記事》Python の組み込み型 dict には、次のメソッドが規定されています。
a.keys()
変数 a が dict 型の値を束縛するとき、そのキー要素をもとにした、list 型の値が得られます。□
def rng(m):
"""
rng m
; map A to B -> set of B
;
; Range
; yields the range (the set of information values) of
; m.
"""
return VDM_Set(m.dict.values())
関数 rng は、写像 m の値集合を生成して、これをリターン値とします。
《関連記事》Python の組み込み型 dict には、次のメソッドが規定されています。
a.values()
変数 a が dict 型の値を束縛するとき、その値要素をもとにした、list 型の値が得られます。□
《ひよ子のきもち♪2008/08/23》
