VDM-SL早見表 [定義]

トップレベル定義

フラットな仕様またはモジュール内の各セクションで定義する
セクション 概要 構文 例
types 型エイリアス 型名 = 型 inv パターン == 条件式;
不変条件inv パターン == 条件式は省略可
 ペア = nat * nat;
ペア = nat * nat inv mk_(x, y) == x + 1 = y;
ペア = nat * nat inv p == p.#1 + 1 = p.#2;
レコード定義 型名:: フィールド名:型 フィールド名:型... inv パターン == 条件式;
フィールド名:は省略可
不変条件inv パターン == 条件式は省略可
 点 :: x:real y:real;
第1象限 :: x:real y:real inv mk_第1象限(x, y) == x >= 0 and y >= 0;
第1象限 :: x:real y:real inv p == p.x >= 0 and p.y >= 0;
values 定数定義 変数:型 = 式;
:型は省略可
 PI : real = 3.141592653589793238
PI2 : real = PI * 2
functions 関数仮定義 関数名: 型 * ... * 型 -> 型
関数名(パターン,...,パターン) == is not yet specified
pre 条件式
p post 条件式
measure 関数名
 pre 条件式およびpost 条件式は省略可
measure 関数名は再帰関数の時のみ、かつ、省略可
 mid : real * real -> real
mid(x, y) == is not yet specified
pre x <= y
post x <= RESULT and RESULT <= y;
陽関数定義 関数名: 型 * ... * 型 -> 型
関数名(パターン,...,パターン) == 式
pre 条件式
post 条件式
measure 関数名
 pre 条件式およびpost 条件式は省略可
measure 関数名は再帰関数の時のみ、かつ、省略可
 mid : real * real -> real
mid(x, y) == (x + y) / 2
pre x <= y
post x <= RESULT and RESULT <= y;
state 状態定義 state 状態空間名 of
    変数名:型
    変数名:型
    ...
inv パターン == 条件式
init 変数パターン == 変数パターン = mk_状態空間名(式,...,式)
end

inv パターン == 条件式は省略可 		state カーソル of
    col : nat
    row : nat
inv mk_カーソル(x, y) == x < 80 and y < 25
init s == s = mk_カーソル(0, 0)
end
operations 純粋操作仮定義 pure 操作名: 型 * ... * 型 ==> 型
操作名(パターン,...,パターン) == is not yet specified
pre 条件式
post 条件式

引数がない場合は型 * ... * 型は()とする。
pre 条件式およびpost 条件式は省略可
 pure カラム位置: () ==> nat
カラム位置() == is not yet specified
post RESULT = col;
純粋操作定義 pure 操作名: 型 * ... * 型 ==> 型
操作名(パターン,...,パターン) == is not yet specified
pre 条件式
post 条件式
 引数がない場合は型 * ... * 型は()とする。
pre 条件式およびpost 条件式は省略可
 pure カラム位置: () ==> nat
カラム位置() == return col
post RESULT = col;
陽操作仮定義 操作名: 型 * ... * 型 ==> 型
操作名(パターン,...,パターン) == is not yet specified
pre 条件式
post 条件式

引数がない場合は型 * ... * 型は()とする。
返値がない場合は==> 型は==> ()とする。
pre 条件式およびpost 条件式は省略可
 カラム移動: int ==> ()
カラム移動(dx) == 文
pre
    let x == カラム位置() + dx
    in (y >= 0 and y < 80)
post cur~ + x = cur;
陽操作定義 操作名: 型 * ... * 型 ==> 型
操作名(パターン,...,パターン) == 文
pre 条件式
post 条件式
 引数がない場合は型 * ... * 型は()とする。
返値がない場合は==> 型は==> ()とする。
pre 条件式およびpost 条件式は省略可
 カラム移動: int ==> ()
カラム移動(dx) == cur := cur + dx
pre
    let x == カラム位置() + dx
    in (y >= 0 and y < 80)
post cur~ + x = cur;

局所定義

種別 概要 構文 例
式 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)
文 let文 let パターン:型=式,...,パターン:型=式 in 文
:型は省略可
 let x:nat = 1 in return x + 1
let x = 1 in return := x + 1
let x:nat = 1, y:nat = 2 in return 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 return x
let b1, b2:bool be st b1 => b2 in return mk_(b1, b2)
ブロック変数 (dcl 変数:型=式,...,変数:型=式; 文; ...)
=式は省略可 		(dcl tmp:nat := v1; v1 := v2; v2 := tmp)
整数forループ for 変数 = 整数式 to 整数式 by 整数式 do 文
by 整数式は省略可
 for i = 1 to 10 do s := s ^ [i]
列forループ for パターン in 列式 do 文
 for i in [1,2,3,4,5] do s := s ^ [i]
集合forループ for all パターン in set 集合式 do 文
 for all i in set {1,...,10} do s := s ^ [i]

パターン

型 概要 構文 例
任意の型 変数 変数 let x = 1 in x + 2
無視 - let - = 1 in 2
値 リテラル
(式)
 cases 4 mod 2: 0 -> <偶数>, 1 -> <奇数> end
組型 組パターン mk_(パターン,...,パターン) let mk_(x, y) = mk_(1, 2) in x + y
レコード型 レコードパターン mk_コンストラクタ(パターン,...,パターン) let mk_Point(x, y) = mk_Point(1, 2) in x + y
集合型 集合外延パターン {パターン,...,パターン} let {x, y} = {1, 2} in x + y
集合併合パターン パターン union パターン let {x} union {1, 3} = {1, 2, 3} in x
列型 列外延パターン [パターン,...,パターン] let [x, y] = [1, 2] in x + y
連結パターン パターン ^ パターン let x^[3] = [1,2,3] in x
写像型 写像外延パターン [パターン |-> パターン,...,パターン |-> パターン] let {2 |-> -, 1 |-> x} = {1 |-> 2, 2 |-> 3} in x
写像併合パターン パターン munion パターン let - munion {1 |-> x} = {1 |-> 2, 2 |-> 3} in x

束縛

型束縛 パターン:型
ただし型はboolなど有限な型に限る。
 {mk_(b1, b2) | b1, b2:bool}
{ x | x : <グー> | <チョキ> | <パー> }
集合束縛 パターン in set 集合式 {mk_(b1, b2) | b1, b2 in set {true, false}}
{ x | x in set {<グー>, <チョキ>, <パー>}}