Python.use(better, VDM++) #forall -- Quantified Expression
‖記事一覧‖
forall -- Quantified Expression
《著》小粒ちゃん+∞《監修》小泉ひよ子とタマゴ倶楽部
第0版♪2000/04/03 ● 第1版♪2003/05/23 ● 第2版♪2006/10/01 ● 第3版♪2009/10/07
事例:モジュールを起動する
■ 全項目を確認する
全ステップの「項目」を確認するには、関数 do を利用します。
$ python -i VDM.py >>> do() 0: step00 -- def VDM_set(): ... >>>
>>> help(forall) ... forall(bind, expr) forall mbd1, mbd2, ..., mbdn & e ; ; Universal quantification ; where each mbdi is a multiple bind pi in set s (or if it ; is a type bind pi : type), and e is a boolean expression ; involving the pattern identifiers of the mbdi's. It has ; the value true if e is true when evaluated in the context ; of every choice of bindings from mbd1, mbd2, ..., mbdn and ; false otherwise.
束縛 bind に含まれる要素の「すべて」が論理式 expr を満たすかを判定した結果が得られます。
■ 各項目を実行する
各ステップの「動作」を確認するには、関数 do に実引数を指定します。
>>> do(@) >>> # -------------------------------------------------- forall >>> s = VDM_set("ABC"); s {'A', 'B', 'C'} >>> [ord(e)%2 for e in s] [1, 0, 1] >>> >>> # forall mbd1, mbd2, ..., mbdn & e >>> s.forall(lambda e: ord(e)%2) False >>> forall(s, 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