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

‖記事一覧‖ Python.use(better, VDM++)《復刻版》

inverse -- map inverse

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

VDM++ に準拠する操作を実現することで、Python との相互理解を深めます。
※ Python1.5 で作成した例題を、Python3.1 で再構成しました。

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

■ 全項目を確認する

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

$ python -i VDM.py
>>> do()
@: tips_inverse -- def inverse(m):
...
>>>

>>> help(inverse)
...
inverse(m)
    inverse m
        ; inmap A to B -> inmap B to A 
        ;
        ; Map inverse
        ;   yields the inverse map of m. m must be a 1-to-1 
        ;   mapping.
■ 各項目を実行する

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

>>> do(@)
>>> # -------------------------------------------------- inverse
>>> m = VDM_map({"A":1,"B":2,"C":3}); m
{'A' |-> 1, 'C' |-> 3, 'B' |-> 2}
>>> inverse(m)
{1 |-> 'A', 2 |-> 'B', 3 |-> 'C'}
>>> m = VDM_map({"A":1,"B":2,"C":1}); m
{'A' |-> 1, 'C' |-> 1, 'B' |-> 2}
>>> inverse(m)
AssertionError: inverse m: m must be a 1-to-1 mapping
	not `1` in {1: 'A'}
>>> 
>>> m = VDM_map({"A":1,"B":2,"C":3}); m
{'A' |-> 1, 'C' |-> 3, 'B' |-> 2}
>>> m.comp(inverse(m))
{1 |-> 1, 2 |-> 2, 3 |-> 3}
>>> inverse(m).comp(m)
{'A' |-> 'A', 'C' |-> 'C', 'B' |-> 'B'}

逆写像が得られます。

事例：コードの解説

》こちらに移動中です《

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/11/18