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

Python VDM++

‖記事一覧‖

exists -- 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(exists)
...
exists(bind, expr)
    exists mbd1, mbd2, ..., mbdn & e 
        ;
        ; Existential quantification
        ;   where the mbdi's and the e are as for a universal
        ;   quantification. It has the value true if e is true when
        ;   evaluated in the context of at least one choice of
        ;   bindings from mbd1, mbd2, ..., mbdn, and false otherwise.

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

■ 各項目を実行する

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

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

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

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

事例：コードの解説

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