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

数値

nat1natintrealであることに注意。
整数型 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)と似た使われ方がされるが、いくつかの点で異なる。
引用型 <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 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 {}

列(リスト)

順序付けられた値の列を扱う型。
列型 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)