VDM-SL早見表 [文]

ブロック

複数の文を逐次実行する文
ブロック文（逐次実行） (dcl 変数:型:=式,...; 文;...;文)
dcl 変数:型:=式,...;は省略可
:=式は省略可
 (dcl tmp:nat := v1; v1 := v2; v2 := tmp)

スキップ

何もしない文
スキップ文 skip while 何か処理をして終了ならfalseを返す() do skip

代入

変数に値を代入する文
代入文 左辺 := 式 x := x + 1
p.x := p.x + 1
ps(3).x := ps(2).x + 1
アトミック代入文 atomic(代入文;...;代入文) atomic(x := x + 1; y := y - 1)
左辺
変数名 変数 x := x + 1
フィールド参照 左辺.フィールド名 p.x := p.x + 1
ps(3).x := ps(2).x + 1
適用参照 左辺(式) ps(3) := ps(2)
car.wheels(3) := wheel

操作呼び出し

操作の呼び出しと復帰を構成する文
呼び出し文 操作名(式,...,式) inc()
add(2)
リターン文 return
return 式
 return
return x + y

分岐

条件分岐をする文
if文（真偽値による場合分け） if 条件式 then 文 else 文
if 条件式 then 文 elseif 条件式 then 文 ... else 文
 if 3 mod 2 = 0 then return <偶数> else return <奇数>

if 10 mod 15 = 0 then return <フィズバズ>
elseif 10 mod 5 = 0 then return <バズ>
elseif 10 mod 3 = 0 then return <フィズ>
else return 10
cases文（パターンマッチによる場合分け） cases 式: パターン,..,パターン -> 文,...,パターン,...,パターン -> 文, others -> 文 end
デフォルト定義, others -> 文は省略可
 cases mk_('+', 1, 2):
  mk_('+', x, y) -> return x + y,
  mk_('-', x, y) -> return x - y,
  others -> return <エラー>
end

cases "03-123-4567":
  市外局番^"-"^市内局番^"-"^下4桁 -> return mk_(市外局番, 市内局番, 下4桁),
  others -> return <エラー>
end

繰り返し

繰り返し処理を行う文
whileループ while 条件式 do 文
 while not 終了() do 処理()
整数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文（局所定義） 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 return 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)