VDM-SL早見表 [型]

• 型
• 表現式
• 定義
• 文

比較

等号や非等号の左右の値の型が合っていなければならないことに注意。

等値	=	? * ? -> bool	1 = 1 1 = 2 1 = '1' '1' = '1' 1 = 1.0
非等値	<>	? * ? -> bool	1 <> 1 1 <> 2 1 <> '1' '1' <> '2' 1 <> 1.0
＞	>	real * real -> bool	1 > 1 2 > 1
≧	>=	real * real -> bool	1 >= 1 1 >= 2
＜	<	real * real -> bool	1 < 1 1 < 2
≦	<=	real * real -> bool	1 <= 1 2 <= 1

数値

nat1 ⊂ nat ⊂ int ⊂ realであることに注意。

• 整数の値は全て実数の値でもある。
• 実数の計算結果の小数点以下がたまたま0である値は整数。

整数型	int	is_int(-1) is_int(1.0) is_int(3.0e8) is_int(1.01)
自然数型	nat	is_nat(1) is_nat(0) is_nat(-1)
正自然数型	nat1	is_nat1(1) is_nat1(0)
実数型	real	is_real(1) is_real(-3.14)

整数リテラル	2 -1
実数リテラル	-3.14 3.0e8 1.0 = 1

加算	+	real * real -> real	1 + 2
減算	-	real * real -> real	1 - 2
乗算	*	real * real -> real	1 * 2
除算	/	real * real -> real	1 / 2 1 / 0
累乗	**	real * real -> real	2 ** 3
商	+	int * int -> int	1 div 2 1 div 0
剰余1	mod	int * int -> int	1 mod 2 -1 mod 2 1 mod -2 1 mod 0
剰余2	rem	int * int -> int	1 rem 2 -1 rem 2 1 rem -2 1 rem 0
絶対値	abs	real -> real	abs 2 abs -1
符号反転	-	real -> real	- 3.14 -(2 + 3)
底	floor	real -> int	floor 3.14 floor -3.14

真偽値

真偽値型

bool

is_bool(true) is_bool(false)

リテラル	true false

and, or, =>は評価順序があり、左側の値で結果が確定する時には右側の式は評価しないことに注意。

否定	not	bool -> bool	not true not false
論理積	and	bool * bool -> bool	true and true true and false true and undefined false and undefined undefined and false
論理和	or	bool * bool -> bool	false or false true or false true or undefined false or undefined undefined or true
含意	=>	bool * bool -> bool	true => true true => false false => false false => undefined undefined => true
同値	<=>	bool * bool -> bool	true <=> true false <=> false true <=> false
非等値(排他論理和)	<>	bool * bool -> bool	true <> true true <> false

文字

文字型

char

is_char('a') is_char('あ')

リテラル	'a' 'あ' '\x41' '\u3012'

文字は等しいかどうかの比較ができるだけで、順序がないことに注意。

等値	=	char * char -> bool	'1' = '1' '1' = '2' 'A' = '\x41'
非等値	<>	char * char -> bool	'1' <> '1' '1' <> '2' 'A' <> '\x41'

引用

引用型は、<と>で囲んだ字面で識別される。多くのプログラミング言語での列挙型(enum)と似た使われ方がされるが、いくつかの点で異なる。

• 単一の値を持つ型で、例えば<引用>の唯一の値は<引用>である。
• 同じ表現が型と値の両方を表す。
• 通常は、ユニオン型と併用して、例えば<引用1> | <引用2>で、<引用1>または<引用2>を値とする型になる。

引用型

<abc>, <引用>, <abc_xyz>

is_(<abc>, <abc>)

リテラル

<abc>) <引用>

等値	=	? * ? -> bool	OK = OK OK = ERROR
非等値	<>	? * ? -> bool	OK <> ERROR OK <> OK

組

多くのプログラミング言語での組（タプル）と似ているが、値の表現がVDM独特であることに注意。

直積型

T1 * T2 * ... * Tn

is_(mk_(1,'a', 3.14), nat * char * real)

コンストラクタ

mk_(1,2) mk_(1,'a',3) mk_(1)

要素の取り出し

mk_(1, 'a', 3).#1 mk_(1, 'a', 3).#2 mk_(1, 'a', 3).#3

オプション / nil

nil になるかもしれない型。

オプション型

[T]

is_(1, [int]) is_(nil, [int])

リテラル

nil

ユニオン型

複数の型にまたがった型。

ユニオン型

T1 | T2 | ... | Tn

is_(1, int | char) is_('a', int | char)

トークン

任意の型の値から、それぞれユニークな値を生成する型

• 内容がどの型の値であっても、トークンの型はtokenになる。
• トークンから中身の値を取り出すことはできない。
• 例えると、絶対に衝突しないハッシュ関数のようなもの

トークン型

token

is_token(mk_token(1)) is_token(mk_token('1')) is_token(mk_token(nil))

コンストラクタ

mk_token(x)

mk_token(1) mk_token("abc") mk_token(nil)

トークンは比較しかできない。トークンの内容が等しい場合、かつその場合のみ、トークンは等しい。

等値	=	token * token -> bool	mk_token(1) = mk_token(2-1) mk_token(1) = mk_token(2) mk_token(1) = mk_token(true)
非等値	<>	token * token -> bool	mk_token(1) <> mk_token(2-1) mk_token(1) <> mk_token(2) mk_token(1) <> mk_token(true)

レコード

多くのプログラミング言語での構造体やレコード型に相当する型。

レコード型

T :: name1:T1 name2:T2 ... namen:Tn T :: T1 T2 ... Tn

コンストラクタ

mk_Point(1, 2.3)

フィールドアクセス

()

mk_Point(1,2).x mk_Point(1,2).y

集合

有限集合を扱う型

集合型	set of T	is_({1,2,3}, set of nat1) is_({}, set of nat1)
非空集合型	set1 of T	is_({1,2,3}, set1 of nat1) is_({}, set1 of nat1)

空集合リテラル	{}
外延表記（列挙）	{1,2,3} {1,2,{'3', nil}}
範囲表記	{1,...,10}
内包表記	{x * 2 | x in set {1, ... ,5}} {x * 2 | x in set {1, ... ,5} & x mod 2 = 0} {mk_(b1, b2, b1 and b2) | b1,b2 : bool}

要素	in set	T * set of T -> bool	1 in set {1,2,3} 0 in set {1,2,3} {1,2} in set {0, {1, 2}, 3}
非要素	not in set	T * set of T -> bool	1 not in set {1,2,3} 0 not in set {1,2,3} {1,2} not in set {0, {1, 2}, 3}
部分集合	subset	set of T * set of T -> bool	{1,2} subset {1,2,3} {1,2,3} subset {1,2,3} {1,2,3} subset {1,2}
真部分集合	psubset	set of T * set of T -> bool	{1,2} psubset {1,2,3} {1,2,3} psubset {1,2,3} {1,2,3} psubset {1,2}
和集合	union	set of T * set of T -> set of T	{1,2} union {2,3}
共通部分	inter	set of T * set of T -> set of T	{1,2} inter {2,3}
差集合	\	set of T * set of T -> set of T	{1,2} \ {2,3}
濃度（要素の数）	card	set of T -> nat	card {1,...,10} card {1, 2, nil} card {}
分配和集合	dunion	set of set of T -> set of T	dunion {{1,2}, {2,3}} dunion {{{1},2}, {2,3}}
分配共通部分	dinter	set of set of T -> set of T	dinter {{1,2}, {2,3}} dinter {{1,2, {3}}, {2,3}}
べき集合	power	set of T -> set of set of T	power {1,2,3} power {}

列（リスト）

順序付けられた値の列を扱う型。

• データ構造は何も規定しない。
• 正自然数インデックスで要素を取り出すことができる。
• 値そのものは immutable である。

列型	seq of T	is_([1,2,3], seq of nat1) is_([], seq of nat1)
非空列型	seq1 of T	is_([1,2,3], seq1 of nat1) is_([], seq1 of nat1)

空列リテラル	[]
外延表記（列挙）	[1,2,3] [1,2,['3', nil]]
文字列リテラル	"文字列" "文字列" = ['文', '字', '列']
内包表記	[x * 2 | x in set {1, ... ,5}] [x * 2 | x in set {1, ... ,5} & x mod 2 = 0]

要素	()	seq of T * nat1 -> T	[0,2,4](2) [0,2,4](10)
スライス	( ,..., )	seq of T * nat1 * nat1 -> T	"任意の文字列"(4,...,5)] "任意の文字列"(5,...,4)] "任意の文字列"(4,...,10)]
先頭要素	hd	seq1 of T -> T	hd [1,2,3] hd "文字列"
続き	tl	seq1 of T -> seq of T	tl [1,2,3] tl "文字列"
長さ	len	seq of T -> nat	len [1,2,3,4,5] len "文字列"
要素集合	elems	seq of T -> set of T	elems [1,2,3,4,5] elems "文字列"
添字集合	inds	seq of T -> set of nat1	inds [0,2,4] inds "文字列"
逆順	reverse	seq of T -> seq of T	reverse [0,2,4] reverse "文字列"
連結	^	seq of T * seq of T -> seq of T	[0,2,4]^[1,3,5] "文字"^"列"
分配連結	conc	seq of seq of T -> seq of T	conc [[0,2,4],[1,3,5]] conc ["文字","列"]
上書き	++	seq of T * map nat1 to T -> seq of T	[0,2,4]++{2|->10} "文字列"++{1|->'数'}]

写像（連想配列、マップ）

多くのプログラミング言語での連想配列やマップ型に相当する型。

写像型	map T1 to T2	is_({1|->'1', 2 |-> '2'}, map nat1 to char) is_({1|->true, 2 |-> false, 3 |-> true, 4 |-> false}, map nat1 to bool)
単射型	inmap T1 to T2	is_({1|->'1', 2 |-> '2'}, inmap nat1 to char) is_({1|->true, 2 |-> false, 3 |-> true, 4 |-> false}, inmap nat1 to bool)

空写像リテラル	{|->}
外延表記（列挙）	{<りんご> |-> 100, <レタス> |-> 200, <大根> |-> 150}
内包表記	{"0123456789"(i+1) |-> i | i in set {0,...,9}} {"0123456789"(i+1) |-> i | i in set {0,...,9} & i mod 2 = 0}

適用	()	map T1 to T2 * T1 -> T2	{0 |-> false, 1 |-> true}(0)
定義域	dom	map T1 to T2 -> set of T1	dom {0 |-> false, 1 |-> true}
値域	rng	map T1 to T2 -> set of T2	rng {0 |-> false, 1 |-> true}
併合	munion	map T1 to T2 * map T1 to T2 -> map T1 to T2	{0 |-> false, 1 |-> true} munion {2 |-> false, 3 |-> true} {0 |-> false, 1 |-> true} munion {1 |-> true, 2 |-> false} {0 |-> false, 1 |-> true} munion {1 |-> false, 2 |-> false}
上書き	++	map T1 to T2 * map T1 to T2 -> map T1 to T2	{0 |-> false, 1 |-> true} ++ {2 |-> false, 3 |-> true} {0 |-> false, 1 |-> true} ++ {1 |-> false, 2 |-> false}
分配併合	merge	set of map T1 to T2 -> map T1 to T2	merge {{0 |-> false, 1 |-> true}, {2 |-> false, 3 |-> true}} merge {{0 |-> false, 1 |-> true}, {1 |-> false, 2 |-> false}}
定義域制限	<:	set of T1 * map T1 to T2 -> map T1 to T2	{2,3} <: {0 |-> false, 1 |-> true, 2 |-> false, 3 |-> true}
定義域除外	<-:	set of T1 * map T1 to T2 -> map T1 to T2	{2,3} <-: {0 |-> false, 1 |-> true, 2 |-> false, 3 |-> true}
値域制限	:>	map T1 to T2 * set of T2 -> map T1 to T2	{0 |-> false, 1 |-> true, 2 |-> false, 3 |-> true} :> {true, nil}
値域除外	:->	map T1 to T2 * set of T2 -> map T1 to T2	{0 |-> false, 1 |-> true, 2 |-> false, 3 |-> true} :-> {true, nil}
合成	comp	map T2 to T3 * map T1 to T2 -> map T1 to T3	{true|-><奇数>, false|-><偶数>} comp {0 |-> false, 1 |-> true, 2 |-> false, 3 |-> true}
繰り返し	**	map T1 to T1 * nat -> map T1 to T1	{0 |-> 1, 1 |-> 2, 2 |-> 3, 3 |-> 3} ** 1 {0 |-> 1, 1 |-> 2, 2 |-> 3, 3 |-> 3} ** 2 {0 |-> 1, 1 |-> 2, 2 |-> 3, 3 |-> 3} ** 3
逆写像	inverse	inmap T1 to T2 -> inmap T2 to T1	inverse {0 |-> '0', 1 |-> '1', 2 |-> '2'}

関数

VDMは関数も型であり、値として扱うことができるが、扱いには注意が必要。

関数型	->	T1 * T2 * ... * Tn -> T
全域関数型	+>	T1 * T2 * ... * Tn -> T

関数定義の他、ラムダ式を関数の値として使うことができる。

関数定義	加算 加算(1,2)
ラムダ式	(lambda x:real, y:real & x + y)(1, 2)