VDM-SL早見表 [式]

局所定義

局所的な定義をする式
let式（局所定義） let パターン:型=式,...,パターン:型=式 in 式
:型は省略可
 let x:nat = 1 in x + 1
let x = 1 in x + 1
let x:nat = 1, y:nat = 2 in x + y
let f:nat -> nat1 f(x) == x + 1 in f(2)
let be式（条件マッチ局所定義） let 多重束縛 be st 条件式 in 式
 let x in set {1,2,3,4} be st x mod 2 = 0 in x
let b1, b2:bool be st b1 => b2 in mk_(b1, b2)

場合分け

場合分けをする式
if式（真偽値による場合分け） if 条件式 then 式 else 式
if 条件式 then 式 elseif 条件式 then 式 ... else 式
 if 3 mod 2 = 0 then <偶数> else <奇数>
if 10 mod 15 = 0 then <フィズバズ> elseif 10 mod 5 = 0 then <バズ> elseif 10 mod 3 = 0 then <フィズ> else 10
cases式（パターンマッチによる場合分け） cases 式: パターン,..,パターン -> 式,...,パターン,...,パターン -> 式, others -> 式 end
デフォルト定義, others -> 式は省略可
 cases mk_('+', 1, 2):
  mk_('+', x, y) -> x + y,
  mk_('-', x, y) -> x - y,
  others -> <エラー>
end
cases "03-123-4567":
  市外局番^"-"^市内局番^"-"^下4桁 -> mk_(市外局番, 市内局番, 下4桁),
  others -> <エラー>
end

比較

等号や非等号の左右の値の型が合っていなければならないことに注意。
等値 = ? * ? -> 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

数式

加算 + 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

論理式

否定 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

要素の取り出し

組 組.#自然数リテラル mk_(1, 'a', 3).#1
mk_(1, 'a', 3).#2
mk_(1, 'a', 3).#3
レコード レコード.フィールド名 mk_Point(1,2).x
mk_Point(1,2).y

適用

列（リスト） 列式(自然数式) [0,2,4](2)
[0,2,4](10)
写像（連想配列、マップ） 写像式(式) {0 |-> false, 1 |-> true}(0)
関数（ラムダ式を含む） 関数式(式,式,...,式) (lambda x:nat & x + 1)(2)
操作 操作()
操作(式,式,...,式)
 inc()
add(2)

コンストラクタ

組 mk_(式,式,...,式) mk_(1,2,3)
mk_("abc", nil, 1)
トークン mk_token(式) mk_token(1)
mk_token("abc")
mk_token(nil)
レコード mk_コンストラクタ(式,式,...,式) mk_Point(1, 2.3)

外延表記（列挙）

集合 {}
{式,式,...,式} 		{}
{1,2,3}
{1,2,{'3', nil}}
{1,...,10}
列（リスト） []
[式,式,...,式]
"文字列"
 []
[1,2,3]
[1,2,['3', nil]]
"文字列"
"文字列" = ['文', '字', '列']
写像（連想配列、マップ） {|->}
{式 |->式 ,式 |-> 式,...,式 |-> 式} 		{|->}
{<りんご> |-> 100, <レタス> |-> 200, <大根> |-> 150}

内包表記

集合 {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}
列（リスト） [x * 2 | x in set {1, ... ,5}]
[x * 2 | x in set {1, ... ,5} & x mod 2 = 0]
写像（連想配列、マップ） {"0123456789"(i+1) |-> i | i in set {0,...,9}}
{"0123456789"(i+1) |-> i | i in set {0,...,9} & i mod 2 = 0}

集合演算

要素 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 * 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|->'数'}]

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

定義域 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'}

量化

多くの組み合わせに関する特性を書く式
全称式（あらゆる） forall 多重束縛,...,多重束縛 & 式 forall i in set {1,2,3} & i mod 4 <> 0
forall i in set {1,2,3} & i mod 2 <> 0
forall b1,b2:bool & b1 or b2
存在式（少なくとも1つ） exists 多重束縛,...,多重束縛 & 式 exists i in set {1,2,3} & i mod 4 = 0
exists i in set {1,2,3} & i mod 2 = 0
exists b1,b2:bool & b1 and b2
ユニーク存在式（1つだけ） exists1 束縛 & 式 exists1 i in set {1,2,3} & i mod 2 = 0
exists1 i in set {1,2,3} & i mod 2 <> 0
exists1 mk_(b1,b2):bool*bool & b1 and b2

イオタ式

集合や型から、条件に合致する唯一の値を取り出す式。 ユニーク存在式と関係が深い。
イオタ式 iota 束縛 & 式 iota i in set {1,2,3} & i mod 2 = 0
iota i in set {1,2,3} & i mod 4 = 0
iota i in set {1,2,3} & i mod 2 = 1

関数

関数を表す式
ラムダ式 lambda 引数:型,...,引数:型 & 式 (lambda x:real, y:real & x + y)(1,2)
(lambda x:real & lambda y:real & x + y)(1)(2)

型判別

値の型を判別する式
一般is式 is_(式, 型) is_(10, nat1)
is_(3.14, nat1)
is_(10, real)
is_({1,...,10}, set of nat1)
基本型is式 is_型(式) is_nat1(10+20)
is_nat1(3.14)
is_real(10)
is_token(mk_token("abc"^"xyz"))

未定義

未定義値を表す
未定義式 undefined undefined
nil = undefined
{1,2,undefined}
{1,2} union undefined