FAQ

VDM自体やその言語，ツールに関するFAQです．

質問項目は随時追加予定です（最終更新2012/01/26）．リクエストも受け付けております．

目次

位置づけ

どういう状況に対してどういう利用効果が期待できる？

開発上流の成果物（仕様書や設計書）を厳密に記述し，主に実行・テストを通した分析・検証を行うことにより，誤解のもととなるような曖昧さや不正確さ，不整合や誤りなどをより排除するようにします．これにより，非常に大きいことが知られている手戻りのコスト，後の過程になってからの修正のコストの発生を防ぐことを目指します．

かなり単純化したイメージとして，上流での修正コストが10，下流（テスト後）での修正コストが100とします．上流・下流での修正がそれぞれ「50件，10件」のときと「10件，50件」のときでは，コストが1500と5100になります．なお，一般には下流での修正コストはより大きい（10倍では済まない）とされることも多いです．非常におおざっぱには，この効用に対して，VDMで仕様を形式化するコストを検討することになります．

こういったイメージを考えると，上流の成果物に起因する修正が多く発生している状況や，下流での修正コストが大きい状況での効果が特に期待されます．例えば強い動機がある状況として，「チームに外国人がいるから日本語の細かい部分が正確に伝わらない」，「外部仕様書を外注先に渡したり，複数の実装チームに渡したりする」といった状況があるかと思います．

ただし，交通などミッションクリティカルなシステムでは，記述・テストに留まらずより強力な検証手段として，証明やモデル検査を活用する手法・ツールを利用することも多いです．

VDM-SL/VDM++はプログラミング言語じゃないの？

プログラミング言語ではなく，仕様記述のための言語です．ただし言語設計上，様々な詳細度での記述が可能となっているので，プログラムを書くときの気持ちになって詳細な情報を書き出していくこともできてしまいます．対象とする上流の成果物において，決めなくてよいこと・決められないこと（後の実装チームなどに任せること）は何でしょうか．またその結果として，VDMモデルに書かなくてよいこと（もしくは実行・テストのために「仮のモック」などとして書くこと）は何でしょうか．そのことを意識する（さらには方針として明文化したり，フレームワークなどを通して強制したりする）といったことが重要になります．

VDMの欠点・限界は？

要求抽出・要求分析や，仕様定義の手法とは補完関係にあります．例えば下記のようなことは目的ではなく，別途検討する必要があります．

形式手法の一つとしてはライトウェイトで，目的によってはそぐいません．他の手法・ツールと比べると主に以下のような特徴があります．

活用

VDM-SLとVDM++の違い（言語上・ツール上）は？どちらを使えばよい？

オブジェクト指向に基づいたモデル化・記述を行いたい場合はVDM++，そうでない場合はVDM-SLということになります（C++やJavaと，Cとの対比と同様）．ただし，スレッド記述やUMLとの相互変換等新しい記述・機能はVDM++のみに追加されている場合が多いので，それらを用いたい場合はVDM++を用いるとよいでしょう．

なお，VDM-SLで（設計のことを気にせずに）要求仕様を明確にした後に，改めてVDM++でオブジェクト設計を意識した記述を行う，といった利用法もあります．

コード生成は使える？生成されたコードが気に入らない

一般的に，VDMで記述するような仕様の情報から実際の実装コードに至る際には，様々な（非機能的）要求が反映されると思います．例えば，実行効率，既存コードの再利用，類似したプロジェクトや派生開発，要求変更に備えた再利用性やメンテナンス性といったことを考慮して，実際の記述を行う方針が議論，選択，決定されると思います．その過程を飛ばして自動化しようとすれば，基本的にはそういった非機能要求を満たすとは限らない「一般的によさそうなコード」を生成することになるでしょう．このため，もし様々な非機能要求を期待しているなら，コード生成はその目的に対して「使えない」という結論になるかもしれません．一方，「とにかく早く動かし始めたい」「プロトタイピング用」ということであれば「使える」のかもしれません．

なお，VDM自体においては理論上，Bメソッドのように，そういった様々な実装方針を少しずつ反映しながら（かつ正当性をその都度確認しながら）実装に近づけていく段階的詳細化を考えることもできます．その場合，最後に自動生成されたコードは非機能要求を満たすようにできるかもしれません．ただし，現時点での言語・ツールはあまり段階的詳細化を行うことを前提としていません．

文法・記述

セミコロンを打つべき場所がわからない

まず，複数の文を順次実行するブロック文内では，各文の終わりにセミコロンを付けます（元々はブロック文内の最後の文には付けないのですが，今のツールでは付けてもエラーにはなりません）．また，操作の定義等それぞれの最後に付けます．

operations
op1 : int ==> int
op1(x) == (
 x := x + 1; -- ブロック文内の各文の最後に付ける
 return p; -- 一番最後の文には付けなくても実はよい
)
pre x < 0; -- （もしあるなら）事前・事後条件も書いてから最後にのみ付ける

op2 : () ==> int
op2() == return a -- ブロック文内でも操作の終わりでもないのでここに付けるとエラー
pre a < 0; -- （もしあるなら）事前・事後条件も書いてから最後にのみ付ける

予期せぬ場所で操作の実行が終わってしまう・「実行されない文」という警告が出る

VDMの意味論では，ブロック文内に戻り値がある操作の呼び出しを行う文があると，その操作の戻り値がreturnされると解釈されてしまいます．一時変数（dcl）や一時定数（def）を用いて無意味な代入をして回避して下さい．

op1(x) == (
  ...
  y := op2(); -- 戻り値を代入に用いたりしていると問題ない
  op3(); -- op3に戻り値があると return op3() と同じ結果になってしまう
  ...
)

回避の具体例は，IOライブラリの説明において載せています．

関数と操作の違いは？使い分けは？

状態（VDM++の場合static変数やインスタンス変数）を読み書きせず入力（引数）だけで出力（戻り値）が定まるものを関数と呼びます．状態を読み書きするものを操作と呼びます．この区別は本来，副作用がない部分はそうと宣言しておくと何かと分析の際に便利であるために導入されたものと思われます．一方，実行してテストする，というくらいの使い方だとあまり区別する必要がありません．

ここで，関数の定義は関数型の記法で行わなければならないので，関数型プログラミング等の経験がないと難しいかもしれません．このため便宜上，（書き慣れた手続き型での）操作ですべて書いてしまうという選択肢もあると思います．一方で，関数の方が多相関数・ラムダ式と強力な表現能力を持っていますので，それらを使いたいときには便宜上関数を使う必要があります．

let式・文とdef式・文の違いは？使い分けは？

どちらも一時定数（一時変数ではない）を定義して用いるものですが，letは状態変数を扱わず（関数型の記述），defは状態変数を扱えるということにされています．この区別は本来，副作用がない部分はそうと宣言しておくと何かと分析の際に便利であるために導入されたものと思われます．しかし現状ツール側で厳密に区別されておらず，どちらを使っても変わらないようです．ただし，文法が微妙に違うので注意して下さい．

関数定義内のmeasureって何？・「measureを再帰関数に定義していない」という警告が出る

再帰関数（自分自身を呼び出す関数）を定義する場合，無限呼び出しに陥らないことを確認（証明）すべきです．その際の方法として，「再帰関数が自分自身を呼び出す際に，ある自然数の指標値が必ず減少し，それがある最小値に到達すれば再帰呼び出しはそれ以上起こらず終了する」ことを証明します．measureはその指標の定義を与えます．Overture IDEにおいては，実行の際にその値が減少していることの動的チェックを行います．

例えば引数として文字列を受け取り，その先頭文字に対して何か処理を行い，残り部分に対して自分自身を呼び出すような再帰関数を考えてみます．

fun : seq of char => seq of char
fun(s) ==
  if len s = 0 then []
  else calc(hd s) ^ tl s;

この関数では再帰呼び出しの度に，引数の文字列の長さが1ずつ小さくなります．引数の文字列の長さが0になったところで，それ以上再帰呼び出しを行わず処理を終了するようにしています．この場合，measureは「引数の文字列の長さ」となります．

VDMにおける具体的な記述の詳細はマニュアル等での記述例をご参照下さい．

VDM++におけるアクセス修飾子には何がある？省略時は？

public，protected，privateはJavaなどのオブジェクト指向プログラミング言語と同様です．すなわち，それぞれ，どのクラスからも参照可能，子孫クラスからのみ参照可能，他クラスから参照不可能です．省略時にはprivateとなります．Javaにおけるパッケージのような概念はありません．現在のツール実装（VDMTools，Overture IDE）では，ツールに読み込ませたクラスはpublic要素を互いに参照可能になります．

ツール利用

VDMToolsとOverture IDEどちらを用いればよい？

特に初心者の場合，Overture IDEのエディタにおけるオンラインでの文法チェックはほぼ必須かと思います．またEclipseに慣れている人もOverture IDEのプロジェクト管理やデバッグは扱いやすいでしょう．一方で，Overture IDEの動作がまだ不安定，または機能が未実装ということもあります．特にUMLとの相互変換やコード生成など比較的高度な機能を試してみたいときは，VDMToolsを利用するとよいと思います．

VDMToolsとOverture IDEをうまく併用するには？

専用エディタ機能のあるOverture IDEを活用していて，記述したものに対してVDMToolsの機能を用いたい場合，Overture IDEからVDMToolsを起動する（プロジェクト内のファイル一式をVDMToolsで開く）機能があります．メニューのWindowからPreferencesを選び，VDM内でVDMToolsのGUIアプリケーションの実行ファイルのパスを指定しておいて下さい．これでプロジェクトのコンテキストメニュー（右クリック）の，"VDM Tools"から，そのプロジェクトで読み込んだファイル一式をVDMToolsに読み込ませて開くことができます．

仕様記述ファイルの拡張子は何にすればよい？ツールごとに拡張子が違う？

Overture IDEの場合，VDM-SL記述は .vdmsl ，VDM++記述は .vdmpp とする必要があります．VDMToolsの場合，記述例やライブラリの拡張子はそれぞれ .vdm ， .vpp とされていますが，ツールは .vdmsl や .vdmpp も読み込み対象としています．このためOverture IDEのものにそろえてしまうのがよいかもしれません．

標準入出力やファイル入出力を使いたい・標準ライブラリやVDMUnitの利用法がわからない

ツールの利用方法で，標準ライブラリ（特に入出力）とVDMUnitそれぞれについて解説しています．

ツール利用（Overture IDE限定）

エディタに記述補完機能はないの？

Eclipseで一般的な，変数名などの補完は Alt+/ で行います．

Eclipseで一般に補完に使われている Ctrl+Space を押すと，テンプレート挿入機能が呼び出されます．例えば op と打って Ctrl+Space を押すと，操作定義（陰定義または陽定義）のテンプレートが挿入できます．メニューのWindowからPreferencesを選び，VDM内のTemplatesから利用可能なテンプレート一覧を見ることができます．

仕様の実行方法がよくわからない（Overture IDE）

基本的な使い方（Overture IDE）を見て下さい

"Open Project in VDM Tools"といったコマンドを選んでも何も起きない

「VDMToolsとOverture IDEをうまく併用するには？」をご参照下さい．

ツール利用（VDMTools限定）

仕様記述ファイルをどうやって編集するの？

VDMTools内にはエディタがありません．外部エディタを使って下さい．変更時には自動でVDMTools側に再読み込みされます．オプションにおいて，VDMTools側から特定の外部エディタを起動するようにも設定できます．

仕様の実行方法がよくわからない（VDMTools）

基本的な使い方（VDMTools）を見て下さい

スクリプトファイルを相対パスで指定したい・清書やコード生成の結果がどこに出てきたのかわからない

インタプリタ上でdirコマンドを使うと，特定のフォルダをパスに追加できます．もしくは，プロジェクトを保存すると，prjファイルを保存したフォルダもパスに追加されます．スクリプトファイル等は，絶対パスでの指定のほか，パス上のフォルダからの相対パスでも指定できます．また，Javaコード生成等の結果は，最後に追加したパスに出力されます．このため，プロジェクトを保存せずにコード生成すると，VDMToolsのインストールフォルダ内のbinフォルダに生成結果が出てきてしまいます．