本ページの内容はあくまで著者がまとめた「簡単に触ってみる第一歩」（Overture IDE 1.1.0 RC1，VDMTools 8.3.1で確認）ですので，詳細なツール仕様や最新の情報については，各ツールの公式Webサイト・マニュアル等をご確認下さい．
大きな画像は縮小しており，クリックすると大きな画像が表示されます．
ツールの選択
どちらも同様の機能（C0カバレッジの計測，仕様記述中における未実行部分の表示）を提供しています．Overture IDEの方が設定が手軽になっていますが，日本語が（コメントだとしても）入る場合，現状VDMToolsの方がよさそうです．
いずれについてもVDM記述のLaTeXによる清書機能を持っています．この清書では，例えばin set 演算子が∈という記号となるなど，数学的な記法により清書されます．この清書機能において，テストで未実行の部分の表示色を変えたり，カバレッジレポートの表を埋め込んだりすることが可能です．
なお，そもそもVDMと自然言語を併用して仕様を記述することができます．この際には，ファイル内にてLaTeXを記述し，\begin{vdm_al}と\end{vdm_al}で囲まれた範囲に実際のVDM記述を行うようにします．
VDMToolの場合
カバレッジ測定・簡単な確認
最初に，インタプリタ上で tcov reset としてカバレッジ情報をリセットしておきます．その後通常と同様にテスト実行を行います．その後 tcov write vdm.tc とするとカバレッジ情報が集計され書き出されます．書き出されたものは rtinfo vdm.tc として表示することができます．
清書機能との連動
LaTeXへの清書機能と連動して，未実行の部分を赤く表示するようなことが可能です．詳細はマニュアルを確認してください．
Overture IDEの場合
カバレッジ測定・簡単な確認
Run Configurationの画面に"Generate Coverage"というチェックボックスがあるので，それをオンにして実行を行います（デフォルトはオンです）．
この際，プロジェクト内のgenerated/coverageフォルダ内に，実行日時ごとに記録が残されます．生成されたカバレッジ記録ファイル（vdmslcovファイル，vdmppcovファイル）を開くと，実行済の部分・未実行の部分が区別されて（それぞれ緑・赤で塗りつぶされて）表示されます．
ただし本ページ執筆の時点では，日本語（2バイト文字）があると，この塗りつぶしがずれてしまうようです．
清書機能との連動
VDM Explorerウィンドウのプロジェクト名のコンテキストメニュー（右クリック）からプロジェクトのプロパティを開くと，その中にLaTeX生成のオプションとして，カバレッジ（%での数値）を表示する表を含めるかどうかといったオプションが設定できます．
同じくプロジェクトのコンテキストメニューからLatex→PdfLatexとすると，各情報を一通り含むLaTeXファイルが生成されるとともにTeXのコンパイルが実行されます．この際の詳細設定（特に利用するパッケージの設置）については確認中です．
© Fuyuki Ishikawa, National Institute of Informatics, Japan, 2011-