VDM++による形式仕様記述

ツール利用方法の目次に戻る

本ページの内容はあくまで著者がまとめた「簡単に触ってみる第一歩」（Overture IDE 1.1.0 RC1，VDMTools 8.3.1で確認）ですので，詳細なツール仕様や最新の情報については，各ツールの公式Webサイト・マニュアル等をご確認下さい．

大きな画像は縮小しており，クリックすると大きな画像が表示されます．

VDMUnitの取得・取り込み

VDMUnitはVDM++のみで記述され実行可能なフレームワークなので，入出力ライブラリのようにツールに依存したものではありません．各ツールでの取り込み方法は下記となります．

Overture IDEの場合，標準ライブラリの一つとして，新規プロジェクト作成時にインポートするように指定すると取り込まれるようになっています．もしくは，VDM Explorerウィンドウ上のコンテキストメニュー（右クリック）から，Newを選ぶとライブラリを足すという選択肢が出てきます．IOライブラリも必要になるので同時に取り込んでください．
VDMToolsの場合，VDMUnitはVDMToolsのWebサイトから取得します．ツールのインストールフォルダ内にあるIOライブラリも必要になるので取り込んでください．

VDMUnitの利用

通常のXXXUnitフレームワークと同様，下記のような特徴を持ちます．

個々のテストケースの分離・独立化： TestCaseクラスのサブクラスとして実際のテストケースを記述
テストの準備・実行・終了処理を定義： setUp(), runTest(), tearDown()の三つの操作を定義．
テストケースをまとめて実行： TestSuiteクラスに各TestCaseクラスを登録，まとめてテストを実行．
テスト結果の出力手段（標準出力，ファイル等）を定義可能： TestResultクラスに残された記録を最終的に出力，またはTestListener クラスを実装し各テストケースごとに随時出力等
各種アサーション式を確認： assertTrue(exp1 = exp2) 等としてアサーションを記述，成り立たなかったテストを記録（エラーメッセージの定義も可能，assertFalseもある）．

このため，簡単には下記のような手順で用いることになるでしょう．

TestCaseクラスを継承し，setUp, runTest, tearDownの三つの操作を通して各テストケースを定義する．一般にはsetUpにて必要なインスタンス変数を生成し初期化を行い，runTestにて適宜assertTrueまたはasssertFalseによるアサーションをはさみつつテスト動作を行います．tearDownはたいていの場合特に必要ないかもしれません．

class TestCase01 is subclass of TestCase

operations 

public TestCase01 : () ==> TestCase01
TestCase01() ==
  TestCase("T01");

public setUp : () ==> ()
setUp() == (
  ...
);

public runTest : () ==> ()
runTest() == (
  ...
);

public tearDown : () ==> ()
tearDown() == skip;

end TestCase01

TestSuiteクラスのインスタンスを作成し，それに対して作成したTestCaseクラスをaddTest操作を通して登録し，その後run操作を通して実行するような操作を定義します．

class TestRun

operations

public static run : () ==> ()
run() == (
  dcl suite : TestSuite := new TestSuite("Event Manager Test"),
      result : TestResult := new TestResult();
  result.addListener(new PrintTestListener());
  suite.addTest(new TestCase01("T01 - normal execution"));
  ...
  suite.run(result);
);

end TestRun

必要に応じデフォルトのPrintTestListenerクラスを変更し，各テストケースの結果が出力される方法を変更する．また，TestResultクラスに含まれる結果（上記では一時変数result）を取り出して適宜出力する．

ツール利用方法の目次に戻る

VDMUnitの使い方

VDMUnitの取得・取り込み

VDMUnitの利用