Python.use(better, VDM++) #comp -- map composition

Python VDM++

‖記事一覧‖

comp -- map composition

《著》小粒ちゃん＋∞《監修》小泉ひよ子とタマゴ倶楽部
第０版♪2000/04/03 ● 第１版♪2003/05/23 ● 第２版♪2006/10/01 ● 第３版♪2009/10/07

事例：モジュールを起動する

■ 全項目を確認する

全ステップの「項目」を確認するには、関数 do を利用します。

$ python -i VDM.py
>>> do()
@: tips_comp -- def comp(m1,m2):
...
>>>

>>> help(VDM_map.comp)
...
comp(m1, m2)
    m1 comp m2
        ; map B to C * map A to B -> map A to C   
        ;
        ; Map composition
        ;   yields the the map that is created by composing m2 
        ;   elements with m1 elements. The resulting map is a 
        ;   map with the same domain as m2. The information 
        ;   value corresponding to a key is the one found by 
        ;   first applying m2 to the key and then applying m1 
        ;   to the result. rng m2 must be a subset of dom m1.
■ 各項目を実行する

各ステップの「動作」を確認するには、関数 do に実引数を指定します。

>>> do(@)
>>> # -------------------------------------------------- comp
>>> m1 = VDM_map({"A":1,"B":2}); m1
{'A' |-> 1, 'B' |-> 2}
>>> m2 = VDM_map({1:"alpha",2:"beta"}); m2
{1 |-> "alpha", 2 |-> "beta"}
>>> m2.comp(m1)
{'A' |-> "alpha", 'B' |-> "beta"}
>>> 
>>> m1 = VDM_map({"A":0,"B":2}); m1
{'A' |-> 0, 'B' |-> 2}
>>> m2 = VDM_map({1:"alpha",2:"beta"}); m2
{1 |-> "alpha", 2 |-> "beta"}
>>> m2.comp(m1)
AssertionError: m1 comp m2: rng m2 must be a subset of dom m1
	`{0, 2}`.subset(`{1, 2}`)

合成写像が得られます。

事例：コードの解説

》こちらに移動中です《

VDM/map

Operator Name Type
dom m Domain (map A to B ) → set of A
rng m Range (map A to B ) → set of B
m1 munion m2 Merge (map A to B ) ∗ (map A to B ) → map A to B
m1 ++ m2 Override (map A to B ) ∗ (map A to B ) → map A to B
merge ms Distributed merge set of (map A to B ) → map A to B
s Domain restrict to (set of A) ∗ (map A to B ) → map A to B
s <-: m Domain restrict by (set of A) ∗ (map A to B ) → map A to B
m :> s Range restrict to (map A to B ) ∗ (set of B ) → map A to B
m :-> s Range restrict by (map A to B ) ∗ (set of B ) → map A to B
m(d) Map apply (map A to B ) ∗ A → B
m1 comp m2 Map composition (map B to C ) ∗ (map A to B ) → map A to C
m ** n Map iteration (map A to A) ∗ nat → map A to A
m1 = m2 Equality (map A to B ) ∗ (map A to B ) → bool
m1 <> m2 Inequality (map A to B ) ∗ (map A to B ) → bool
inverse m Map inverse inmap A to B → inmap B to A
  • Note that the types A, set of A and set of set of A are only meant to illustrate

↑TOP


関連記事

Last updated♪2009/10/31