Python.use(better, VDM++) #exists1 -- Quantified Expression

Python VDM++

‖記事一覧‖

exists1 -- Quantified Expression

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

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

■ 全項目を確認する

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

$ python -i VDM.py
>>> do()
0: step00 -- def VDM_set():
...
>>>

>>> help(exists1)
...
exists1(bind, expr)
    exists1 bd & e
        ;
        ; Unique existential quantification
        ;   where bd is either a set bind or a type bind and e is a
        ;   boolean expression involving the pattern identifiers of
        ;   bd. It has the value true if e is true when evaluated in
        ;   the context of exactly one choice of bindings, and false
        ;   otherwise.

束縛 bind に含まれる要素の「ひとつだけ」が論理式 expr を満たすかを判定した結果が得られます。

■ 各項目を実行する

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

>>> do(@)
>>> # -------------------------------------------------- exists1
>>> s = VDM_set("ABC"); s
{'A', 'B', 'C'}
>>> [ord(e)%2 for e in s]
[1, 0, 1]
>>> [not ord(e)%2 for e in s]
[False, True, False]
>>> 
>>> # exists1 bd & e
>>> s.exists1(lambda e: ord(e)%2)
False
>>> exists1(s, lambda e: ord(e)%2)
False
>>> s.exists1(lambda e: not ord(e)%2)
True
>>> exists1(s, lambda e: not ord(e)%2)
True
>>> 
>>> s = VDM_set(); s
{}
>>> s.exists1(lambda e: ord(e)%2)
False

集合 s に含まれる要素 e の「すべて」が、条件式を満たすかを判定した結果が得られます。

  • 条件式 ord(e)%2 を満たさない要素 e が含まれるので、False が得られます。

事例：コードの解説

VDM/set

Operator Name Type
e in set s1 Membership A ∗ set of A → bool
e not in set s1 Not membership A ∗ set of A → bool
s1 union s2 Union set of A ∗ set of A → set of A
s1 inter s2 Intersection set of A ∗ set of A → set of A
s1 \ s2 Difference set of A ∗ set of A → set of A
s1 subset s2 Subset set of A ∗ set of A → bool
s1 psubset s2 Proper subset set of A ∗ set of A → bool
s1 = s2 Equality set of A ∗ set of A → bool
s1 <> s2 Inequality set of A ∗ set of A → bool
card s1 Cardinality set of A → nat
dunion ss Distributed union set of set of A → set of A
dinter ss Distributed intersection set of set of A → set of A
power s1 Finite power set set of A → set of set of 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/26