Python.use(better, VDM++) 記事一覧 - 続・ひよ子のきもち

VDM++ 形式手法への誘い：Python 篇

《著》小粒ちゃん＋∞《監修》小泉ひよ子とタマゴ倶楽部

第０版♪2000/04/03 ● 第１版♪2003/05/23 ● 第２版♪2006/10/01 ● 第３版♪2009/10/07

VDM++ に準拠する操作を実現することで、Python との相互理解を深めます。
※ Python1.5 で作成した例題を、Python3.1 で再構成しました。

7 Expressions

7.3 Unary and Binary Expressions

‘+’ 

    
     ‘-’ 
     ‘abs’ 
     ‘ﬂoor’ 
     ‘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

    
        

    ♪ 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
     Diﬀerence
     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




    ♪ 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 に対する演算（１）

関連記事
集合を要素とする集合
要素の帰属関係
事例：演算 in

2006-10-05 VDM++《4》Set に対する操作（２）

和集合と積集合
事例：演算 union/inter
自己紹介する関数オブジェクト
演算の型を規定する

2006-10-06 VDM++《5》Set に対する操作（３）

差集合
事例：演算 ￥

2006/10/13《10》全称 ★ 伊藤うさぎ
2006-10-23 VDM++《16》Map に対する演算（１）

定義域と値域
事例：演算 dom
事例：演算 rng

2006-10-24 VDM++《17》Map に対する演算（２）

写像の併合
事例：演算 munion
事例：演算 ++
事例：演算 merge

2006-10-25 VDM++《18》Map に対する演算（３）

定義域と値域の限定
事例：演算 <:
事例：演算 <-:
事例：演算 :>
事例：演算 :->



2006-10-26 VDM++《19》Map に対する演算（４）

写像の適用
事例：演算 ()
事例：演算 comp
事例：演算 **

》こちらに移動中です《
↑TOP





    関連記事
    

Python への扉
Last updated♪2009/10/25

‘-’	‘abs’	‘ﬂoor’	‘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’ ;

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	Diﬀerence	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

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

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