Python.use(better, VDM++) #comp -- map composition
‖記事一覧‖ Python.use(better, VDM++)《復刻版》
comp -- map composition
《著》小粒ちゃん+∞《監修》小泉ひよ子とタマゴ倶楽部
第0版♪2000/04/03 ● 第1版♪2003/05/23 ● 第2版♪2006/10/01 ● 第3版♪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