Python.use(better, VDM++) 記事一覧
《著》小粒ちゃん+∞《監修》小泉ひよ子とタマゴ倶楽部
第0版♪2000/04/03 ● 第1版♪2003/05/23 ● 第2版♪2006/10/01 ● 第3版♪2009/10/07
VDM++ に準拠する操作を実現することで、Python との相互理解を深めます。
※ Python1.5 で作成した例題を、Python3.1 で再構成しました。
7 Expressions
7.3 Unary and Binary Expressions
‘+’
‘-’ | ‘abs’ | ‘floor’ | ‘not’ | ||
‘card’ | ‘power’ | ‘dunion’ | ‘dinter’ | ||
‘hd’ | ‘tl’ | ‘len’ | ‘elems’ | ‘inds’ | ‘conc’ |
‘dom’ | ‘rng’ | ‘merge’ ; | |||
‘+’
‘-’ | ‘*’ | ‘/’ | |||
‘rem’ | ‘div’ | ‘mod’ | ‘**’ | ||
‘union’ | ‘inter’ | ‘\’ | ‘subset’ | ||
‘psubset’ | ‘in set’ | ‘not in set’ | |||
‘^’ | |||||
‘++’ | ‘munion’ | ‘ | ‘<-:’ | ‘:>’ | ‘:->’ |
‘and’ | ‘or’ | ||||
‘=>’ | ‘<=>’ | ‘=’ | ‘<>’ | ||
‘<’ | ‘<=’ | ‘>’ | ‘>=’ | ||
‘comp’ ; | |||||
♪ 7.5 Quantified Expressions
- 2005-01-19 Python.use(better, VDM++) #forall -- Quantified Expression
- 2005-01-20 Python.use(better, VDM++) #exists -- Quantified Expression
- 2005-01-22 Python.use(better, VDM++) #exists1 -- Quantified Expressio
♪7.6 The Iota Expression
- iota bd & e
↑TOP♪ 7.7 Set Expressions
- 2005年3月07日(月)
- 2005年3月08日(火)
- 2005-03-09 Python.use(better, VDM++) #union -- union
- 2005年3月10日(木)
- 2005年3月11日(金)
- 2005年3月14日(月)
- 2005年3月15日(火)
- 2005年3月16日(水)
- 2005年3月17日(木)
- 2005年3月18日(金)
- 2005年3月21日(月)
- 2005-03-22 Python.use(better, VDM++) #dinter -- distributed intersection
- 2005-03-23 Python.use(better, VDM++) #power -- finite power 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
♪ 7.8 Sequence Expressions
- 2005年4月18日(月)
- 2005年4月19日(火)
- 2005年4月20日(水)
- 2005年4月21日(木)
- 2005年4月22日(金)
- 2005年4月28日(木) XX
- 2005年4月29日(金)
- 2005年5月02日(月)
- 2005-05-03 Python.use(better, VDM++) #__add__ -- sequence modification
- 2005年5月04日(水)
- 2005年5月05日(木)
- 2005年5月06日(金)
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 |
♪ 7.9 Map Expressions
- 2005年5月09日(月)
- 2005年5月10日(火)
- 2005-05-11 Python.use(better, VDM++) #munion -- merge
- 2005-05-12 Python.use(better, VDM++) #__add__ -- override
- 2005年5月13日(金)
- 2005年5月16日(月)
- 2005年5月17日(火)
- 2005年5月18日(水)
- 2005年5月19日(木)
- 2005年5月20日(金)
- 2005-05-23 Python.use(better, VDM++) #comp -- map composition
- 2005年5月24日(火)
- 2005年5月25日(水)
- 2005年5月26日(木)
- 2005-05-27 Python.use(better, VDM++) #inverse -- map inverse
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 <: m | 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 |
- 2006/10/03《2》Set 集合型★ 河野かえる
- 2006-10-04 VDM++《3》Set に対する演算(1)
- 2006-10-05 VDM++《4》Set に対する操作(2)
- 2006-10-06 VDM++《5》Set に対する操作(3)
- 2006/10/13《10》全称 ★ 伊藤うさぎ
- 2006-10-23 VDM++《16》Map に対する演算(1)
- 2006-10-24 VDM++《17》Map に対する演算(2)
- 2006-10-25 VDM++《18》Map に対する演算(3)
- 2006-10-26 VDM++《19》Map に対する演算(4)