【VDMTools】TCファイルの仕様考察

     VDMToolsにおけるtcファイルの仕様

VDMToolsのtcファイルを使うことによってカバレッジ情報の確認が可能となったが，「どの命令が実行されていて，どの命令が実行されていないのか」については清書機能を用いる必要があった．tcファイルの仕様が不明だったためである．以下，tcファイルのカバレッジに関する部分について理解している範囲で詳述する．

まず，下記のようなVDM++のサンプルコードを用意する．

Sample.vpp

class A

operations

public op: bool ==> nat

op(b) == if b

        then return 1

        else return 2;

end A

次に，このコードに対してop(true)を実行する．

すると，カバレッジは以下のように出力される：

vpp> rtinfo vdm.tc

   66%      1  A`op

さらに，「ni」コマンドを使ことによりコードとカバレッジのマッピング情報を知ることができる．この出力には「ノード」と「トークン」に関する情報が含まれており，3行ごとにノード情報を表す．一行目がノードID，トークンID，カバレッジなどを表し，2行目と3行目はノードの最初と最後のトークンを示しているとのことであった．ここでノードとトークンという用語の定義に対する理解に至っていない．推測では，トークンが文字列，ノードが意味のある文字列のブロック(classやoperationなど)のことを言っていると考えた．

ここで注目すべきは「count」のラベルがついたノードである．ここがカバレッジの集計対象であり，この部分がすべて実行されていれば先で実行したVDM++コードのカバレッジが100%ということになるはずである．この例の場合，以下に記載する部分である：

41943049 ( 16, 16, 16), 1, nil, nil, 0, true, false --> count: 1

( 1,  6,  6,  6, 13),( 1,  6,  6,  6, 14),0,0,426,b

( 1,  6,  6,  6, 13),( 1,  6,  6,  6, 14),0,0,426,b

41943050 ( 19, 19, 19), 1, nil, nil, 0, true, false --> count: 1

( 1,  7,  7,  7, 21),( 1,  7,  7,  7, 22),0,0,433,1

( 1,  7,  7,  7, 21),( 1,  7,  7,  7, 22),0,0,433,1

41943051 ( 18, 18, 18), 2, nil, nil, 0, true, false --> count: 2

( 1,  7,  7,  7, 14),( 1,  7,  7,  7, 20),0,0,401,return

( 1,  7,  7,  7, 14),( 1,  7,  7,  7, 20),0,0,401,return

41943052 ( 22, 22, 22), 0, nil, nil, 0, true, false --> count: 0 <= UNCOV =

( 1,  8,  8,  8, 21),( 1,  8,  8,  8, 22),0,0,433,2

( 1,  8,  8,  8, 21),( 1,  8,  8,  8, 22),0,0,433,2

41943053 ( 21, 21, 21), 0, nil, nil, 0, true, false --> count: 0 <= UNCOV =

( 1,  8,  8,  8, 14),( 1,  8,  8,  8, 20),0,0,401,return

( 1,  8,  8,  8, 14),( 1,  8,  8,  8, 20),0,0,401,return

41943054 ( 15, 15, 20), 1, nil, nil, 0, true, false --> count: 1

( 1,  6,  6,  6, 10),( 1,  6,  6,  6, 12),0,0,348,if

( 1,  8,  8,  8,  9),( 1,  8,  8,  8, 13),0,0,330,else

41943055 ( 15, 15, 22), 0, nil, nil, 0, false, false

( 1,  6,  6,  6, 10),( 1,  6,  6,  6, 12),0,0,348,if

( 1,  8,  8,  8, 21),( 1,  8,  8,  8, 22),0,0,433,2

41943056 (  5,  5, 14), 1, nil, nil, 0, true, false --> count: 1

( 1,  5,  5,  5,  8),( 1,  5,  5,  5, 10),0,0,426,op

( 1,  6,  6,  6,  7),( 1,  6,  6,  6,  9),0,0,360,==

count対象ノードが7，うち実行されているノードが5で，カバレッジは5割7掛ける100，と考えたのだが，結果は66%のなので計算方法が違う．疑問が残るが，ここで見ることのできる情報は「未実行のノード情報」であるので置いておく．未実行のノードについてはUNCOVラベルに注目すれば抽出できそうだ．この例でのUNCOVラベルのついたノードは「２」と「return」である．この出力を処理してユーザへ未実行部分の情報を与えるケースを考えた場合，未実行ノードをばらして見せるのではなく，行数情報や文字数情報を活用し，体裁を整えてから見せたほうが親切だろうと考える．

ここまでの話をまとめる．

【わかったこと】

ž   テストを実行した後，”ni”コマンドによってコードの実行されたノード，実行されていないノードを確認できる

ž   “ni”コマンドの出力には，ノードとトークン情報が含まれており，そのトークンが何行目何文字列目かといったこともわかる

【不明点】

ž   「ノード」「トークン」の正確な定義

ž   カバレッジの算出方法

ž   ノードやトークンに関する情報の正確な読み取り方