VDMを用いた仕様記述・検証 〜 仕様検証編 〜：誰でも使える形式手法（5）（2/3 ページ）

[植木雅幸（CSK），＠IT MONOist]

VDMToolsを用いた仕様の検証

　前ページでは、仕様の検証方法についていろいろと見てきました。

　冒頭でも説明したとおり、VDMでは仕様をテストすることで検証を行います。ここでは、VDMToolsを使ってVDM仕様を検証する方法を紹介します。

　まず、検証の流れを確認してみましょう（図1）。

図1　VDMToolsを用いた検証の流れ

　このテストの一連の流れを繰り返し実施します。これがVDMにおける回帰テストです。

　ここで、「テストカバレッジ」について少し説明しておきましょう。VDMToolsで出力されるテストカバレッジは「C0レベル」です。これは「命令網羅率」ともいわれ、分岐の条件や経路の組み合わせを考えずに、単純に全命令に対して各命令を実行した比率を表します。このテストカバレッジはどれだけ仕様が検証されたかを示します。

　正当性確認では、防衛的な例外仕様など、テスト実行ができないような仕様以外のカバレッジを100％にするのは最低条件といってもよいでしょう。その前提で、さらにテストケースを追加していくことにより、仕様の品質を高めていきます。妥当性検証では、要求に対する仕様の妥当性を検証したときに、そのテストケースが仕様をどの程度検証できているのかを、カバレッジによって確認します。こうすることにより、要求と仕様の間に齟齬（そご）がないかどうかを網羅的に確認できるのです。

　ちなみに、VDMToolsの清書機能を使ってカバレッジ情報を清書すると、図2のように実行した部分と実行していない部分を色分けしたり、図3のように操作・関数単位でカバレッジ率を出力できます。また、RTF形式やTeX形式でカバレッジ情報を出力することが可能です。

図2　清書の例：カバレッジ色分け

図3　清書の例：カバレッジ表

VDMUnit

　VDMで仕様を記述し、VDMToolsを使ってテストする場合、テストケースは自分で記述するだけでなく、テスト実行に至る仕組みも自分自身で用意する必要があります。

　一度仕組みを作ってしまえば、次からはそれを用いるだけで済みますが、できることなら初回も自分では作成したくないものです。なぜなら、VDMで「仕様」を記述することが本来の目的であり、仕様以外の実行に対する仕組み部分は本質から外れるところだからです。

　VDM++には、その仕組みをつかさどる「VDMUnit」というテスト用のフレームワークが存在します。これは、VDM++の教科書「Validated Designs for Object-oriented Systems」（注）の著者である、Marcel Verhoef氏が作成したフレームワークで、Javaの「JUnit」やC++の「CPPUnit」と同じような構成・機能を有しています（図4）。

図4　VDMUnitの構造

※注：「Validated Designs for Object-oriented Systems」は、現在、日本語版出版のために翻訳中です。http://overturetool.org/publications/books/vdoos/

　VDMUnitの利点は、テスト実行に至る仕組みを提供してくれる以外にもあります。それは、同じテストケースを使って簡単に何度もテストをする回帰テストができることです。これは前述（“仕様を検証するということ−テスト”の節）したように、回帰テストをすることにより、仕様変更・追加時の影響範囲特定や、「正しい」状態を保ったまま仕様開発ができる点で高い効果を発揮します。また、VDMUnitのようなテストフレームワークを用いることにより、仕様部分と仕様を動作させる部分を明確に分離できますので、仕様を人に伝えるという面でも効果があります。

　VDMUnitの基礎となるJUnitやCPPUnitのような“xUnitフレームワーク”は、元来単体テスト向けのフレームワークです。しかし、使い方によっては、シナリオベースのシステムテストにも十分使えるものです。そこで、今回はVDMUnitを用いた正当性確認と妥当性確認について解説していきます。

　なお、このVDMUnitはVDM公式サイトで配布していますので、ぜひ試してみてください。

仕様の正当性を検証する

　まずは、正当性確認について説明します。プログラムに対する正当性確認はプログラムの「単体テスト」に当たります。つまり、“作られたプログラムのそれぞれのクラスやモジュール、関数などが、意図したとおりに動作することを検証する”ことです。これは、仕様検証における正当性確認でも変わりません。VDMで記述した仕様のクラスや関数、操作などが意図したとおりに動作するかを検証します。

　この正当性確認には、「同値分割」や「境界値分析」などのテスト工学の技術を使うことができます。つまり、これまで保有していたテストに関する知識や資産を使うことができ、それにより効率的に仕様の検証ができるといったメリットがあります。

　VDMにおける正当性確認のためのテストケースを抽出する方法はいくつかあります。まず1つ目は上記のようにテスト工学の技術を使ったテストケースの抽出方法です。こちらについては、より詳しい情報が書籍やWebサイトなどにありますので、ここでは割愛します。2つ目にVDM特有のテストケース抽出方法として取り上げたいのが、“制約条件からのテストケース抽出”です。

　例として、連載第4回で記述した「ライン制御」クラスの「ライン状態を判定する」操作を検証してみましょう。まず、「ライン状態を判定する」操作は以下のように定義されていました。

 1 :  public ライン状態を判定する : () ==> 「ライン状態」
 2 :  ライン状態を判定する() ==
 3 :    cases i光センサー.黒線レベル値を読み取る():
 4 :      <黒閾値以下> -> return <黒>,
 5 :      <白閾値以上> -> return <白>,
 6 :      others -> return <不明>
 7 :    end
 8 :  pre
 9 :    i光センサー.黒線レベル値を読み取る() <> nil
10 :  post
11 :    cases mk_(i光センサー.黒線レベル値を読み取る(), RESULT):
12 :      mk_(<黒閾値以下>, <黒>) -> true,
13 :      mk_(<白閾値以上>, <白>) -> true,
14 :      mk_(-, <不明>) -> true,
15 :      others -> false
16 :    end; 

　この操作を検証するために、事後条件に注目してみましょう。事後条件は、読み取った黒線レベルの値と、この操作の戻り値の組み合わせになっています。例えば、黒線レベル値が黒閾値以下であれば戻り値は黒です。これをテストケースとして考えると、入力データの黒線レベル値が黒閾値以下のときに、結果が黒であればよいことになります。これをVDMUnitのテストケースとして記述すると以下のようになります。

 1 :  class testVerification01 is subclass of TestCase
 2 :    instance variables
 3 :      public iLineCtrl : 「ライン監視制御」;
 4 :
 5 :    operations
 6 :      public setUp : () ==> ()
 7 :      setUp() ==
 8 :      (
 9 :        iLineCtrl := new 「ライン監視制御」();
10 :        iLineCtrl.黒線レベル値をセットする(<黒閾値以下>);
11 :      );
12 :
13 :      public runTest : () ==> ()
14 :      runTest() ==
15 :      (
16 :        dcl tライン状態 : 「ライン監視制御」`「ライン状態」;
17 :        tライン状態 := iLineCtrl.ライン状態を判定する();
18 :        assertTrue("test01 failed.", tライン状態 = <黒>);
19 :      );
20 :  end testVerification01 

　TestCaseクラスのサブクラスとして新たなテストクラスを作っています（1行目）。そして、7行目のsetUp操作で入力条件を準備しています。今回は<黒閾値以下>です。その後、runTest操作では「ライン状態を判定する」操作を呼び出して、結果を検証しています。このテストケースを、VDMToolsを使ってテストすると、図5のような画面になります。

図5　正当性確認をVDMToolsで実行

　今回はこの一例のみを紹介しましたが、同じようにテストケースを複数実行することで、個々の仕様品質を高めることができます。

　ちなみに、現在VDMToolsの機能拡張として、テストケースの自動生成機能を研究開発しています。正当性確認のテストケースのような単純なテストケースを自動生成することはある程度機械的にできますので、今後のバージョンアップを楽しみにしていてください。