先日ソフトウェアエンジニアリングシンポジウムに提出した分の作業で，
VDMToolsを使用する機会があった．先行研究では主に実行可能なVDM++ファイルを扱っており，VDM++にテストデータを与える形で実行し，想定される結果と実際の出力を比較する．このとき，福次出力としてコードカバレッジ情報（VDM++中の式のちどれくらい実行されたかを示す指標）も出力されており，前回の研究ではこれを扱った．コードカバレッジ情報を整理する上でいくつかポイントとなる点があったので以下に記録しておく．
◆1.1 フレームワークが処理する部分とユーザが処理する部分
フレームワークはVDMToolsが備える仕組みを用いて仕様の実行，結果の確認，コードカバレッジの出力を担う．このとき，コードカバレッジ出力の部分に関しては注意する必要がある．というのも，VDMToolsでコードカバレッジを出力するためにはいくつかのステップがあり，フレームワークはすべてのステップを実行してくれるわけではないからだ．ステップは以下である：
1. テスト対象となるVDM++ファイルを用意し，それをもとにカバレッジファイル(.tc)のブランクファイルを作成する
2. VDM++の実行ファイル(.arg)を用意する
3. VDM++ファイル，実行ファイル，カバレッジファイルを入力とし，テストを実行，カバレッジ情報を.tcファイルへ追記する
4. カバレッジ情報を表示する
5. カバレッジ情報を清書し，VDM++ファイルで実行された式，実行されていない式といった情報を表示する
フレームワークでサポートしているのは3番までである．すなわちテストを実行した後，フレームワークはtcファイルをテストの福次出力としてHDFSへ書き出す．ユーザは，このtcファイルからカバレッジ情報を確認することができる．
◆1.2 各手順でのコマンド
一連の手順をコマンドラインで行う場合，VDM++バイナリとVDMインタープリタを活用することで実現できる．
l 1でカバレッジのブランクを作成するが，これはLinuxのシェルを用いてVDMのバイナリを起動し，例えば以下のように入力する：
l 3でのテスト実行とカバレッジ情報の出力だが，これは同様にVDMバイナリを用いて以下のように入力する：
◆1.1 フレームワークが処理する部分とユーザが処理する部分
フレームワークはVDMToolsが備える仕組みを用いて仕様の実行，結果の確認，コードカバレッジの出力を担う．このとき，コードカバレッジ出力の部分に関しては注意する必要がある．というのも，VDMToolsでコードカバレッジを出力するためにはいくつかのステップがあり，フレームワークはすべてのステップを実行してくれるわけではないからだ．ステップは以下である：
1. テスト対象となるVDM++ファイルを用意し，それをもとにカバレッジファイル(.tc)のブランクファイルを作成する
2. VDM++の実行ファイル(.arg)を用意する
3. VDM++ファイル，実行ファイル，カバレッジファイルを入力とし，テストを実行，カバレッジ情報を.tcファイルへ追記する
4. カバレッジ情報を表示する
5. カバレッジ情報を清書し，VDM++ファイルで実行された式，実行されていない式といった情報を表示する
フレームワークでサポートしているのは3番までである．すなわちテストを実行した後，フレームワークはtcファイルをテストの福次出力としてHDFSへ書き出す．ユーザは，このtcファイルからカバレッジ情報を確認することができる．
◆1.2 各手順でのコマンド
一連の手順をコマンドラインで行う場合，VDM++バイナリとVDMインタープリタを活用することで実現できる．
l 1でカバレッジのブランクを作成するが，これはLinuxのシェルを用いてVDMのバイナリを起動し，例えば以下のように入力する：
$ vppde –p –R vdm.tc sorter.vpp dosorter.vppこのtcファイルはsorter.vppとdosorter.vppに記述されているクラスの情報をもつことになる．
l 3でのテスト実行とカバレッジ情報の出力だが，これは同様にVDMバイナリを用いて以下のように入力する：
$ vppde –i –R vdm.tc sort.arg sorter.vpp dosort.vppl 4でのカバレッジ情報の表示については，VDMインタープリタを起動する．VDMインタープリタはシェルから引数を指定せずにVDMバイナリを呼ぶと起動する：
$vppdeその後，インタープリタにて以下を入力する：
>read sorter.vpp dosort.vpp
>rtinfo vdm.tcまず，tcファイルが持つクラスの情報をインタープリタ内へ取り込む必要がある．rtinfoはカバレッジ情報を出力するためのコマンドで，引数にtcファイルを指定する．結果は下の図のようになる．
l ここで，tcファイルを操作することに関していくつかの機能を紹介する．テストによっては，例えばひとつずつのsorter.vppとdosort.vppに対して複数のargファイルを用意，複数回のテストを実行し，複数のtcファイルが生成される場合がある（フレームワークで複数のMapを生成し並列分散処理を行うとこのような状況が発生する）．散らばったtcファイルに関しては，以下のコマンドを実行するとひとつのファイルに情報を統合することができる：
> read 必要なvppファイル> tcov read vdm1.tc> tcov read vdm2.tc …> tcov write vdm.tctcov write コマンドで，それまでtcovが蓄積したカバレッジ情報を１ファイルに出力することができる．
l 5で，カバレッジ情報を清書して出力する機能を挙げているが，そのコマンドは今度はシェルからで，以下である：
Ø $ vppde –lr sorter.vpp dosort.vpp
清書機能がオプションｒつきで呼び出されると．実行したテストでカバーできていないDoSort, InsertSorted, Sortといった関数や操作の部分にマークがつく．ここで，いくつか注意しなければならないことがある：
Ø このコマンドはvdm.tcという名前のカバレッジファイルに反応する．つまり，清書させたいカバレッジ情報は，vdm.tcという名前にしておく必要がある．
Ø 清書された文書はVDM++ファイルの入力形式に依存する．和田が把握している範囲では，ここで使用できる形式はリッチテキスト(rtf),，Tex，そしてプレーンテキストである．カバーされているもの，されていないものといった情報を得たい場合，VDM++のクラスはリッチテキスト形式，またはTexで記述している必要がある．フレームワークの例として使用されていたエニグマ関連のVDM+＋ファイルはプレーンテキストで記述されていたため，清書してもカバレッジ情報が色分けされておらず手間取った．
ここでの例はTex形式での入力である．よって出力もTexであり，清書されたTexファイルをコンパイルしてPDF形式などにおこすと以下図の右のようになる．また．プレーンテキストの場合，以下図の左のようになる：
今回はリッチテキストが入力となる場合の手順は省略する．
