Python.use(better, VDM++) #__add__ -- sequence modification

Python VDM++

‖記事一覧‖

__add__ -- sequence modification

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

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

■ 全項目を確認する

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

$ python -i VDM.py
>>> do()
@: tips_sequence_modification -- def __add__(s,m):
...
>>>

>>> help(VDM_seq.__add__)
...
__add__(s, m)
    l ++ m
        ; seq of A * map nat1 to A -> seq of A 
        ;
        ; Sequence modification
        ;   the elements of l whose indexes are in the domain of
        ;   m are modified to the range value that the index maps
        ;   into. dom m must be a subset of inds l
■ 各項目を実行する

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

>>> do(@)
>>> # -------------------------------------------------- sequence_modification
>>> s = VDM_seq("ABC"); s
['A', 'B', 'C']
>>> m = VDM_map({2:"b"}); m
{2 |-> 'b'}
>>> s + m
['A', 'b', 'C']
>>> s = VDM_seq("ABC"); s
['A', 'B', 'C']
>>> m = VDM_map({0:"b"}); m
{0 |-> 'b'}
>>> s + m
AssertionError: l ++ m: dom m must be a subset of inds l
	`{0}`.subset.(`{1, 2, 3}`)
>>> s = VDM_seq("ABC"); s
['A', 'B', 'C']
>>> m = VDM_map({4:"b"}); m
{4 |-> 'b'}
>>> s + m
AssertionError: l ++ m: dom m must be a subset of inds l
	`{4}`.subset.(`{1, 2, 3}`)

逆写像が得られます。

事例：コードの解説

》こちらに移動中です《

VDM/seq

Operator Name Type
hd l Head seq1 of A → A
tl l Tail seq1 of A → seq of A
len l Length seq of A → nat
elems l Elements seq of A → set of A
inds l Indexes seq of A → set of nat1
l1 ^ l2 Concatenation (seq of A) ∗ (seq of A) → seq of A
conc ll Distributed concatenation seq of seq of A → seq of A
l ++ m Sequence modification seq of A ∗ map nat1 to A → seq of A
l(i) Sequence application seq of A ∗ nat1 → A
l1 = l2 Equality (seq of A) ∗ (seq of A) → bool
l1 <> l2 Inequality (seq of A) ∗ (seq of A) → bool
  • 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