　前回、「VDMは仕様をテストできる」と説明しましたが、ただやみくもにテストケースを考え、テストをしても、そのテストケースが要求に対して妥当であるかどうかは分かりません。また、「VDMTools（VDMを用いた開発を支援するツール）」によりテストの実行自体は自動化されますが、テストケース記述やテストに至る仕組み（環境）は自分で作る必要があります。テスト環境は仕様記述の本質ではなく、単にテストを実行するためのものですから、容易に環境が作れることが大切であり、その分、テストケースの検討に時間を十分に割くことが理想です。

　上記の目的を達成し、VDMで効果的なテストを実施する手段として、「テストカバレッジの計測」と「テスティングフレームワーク」、VDMToolsインタプリタによる「回帰テスト」を以下で紹介します。

　テストカバレッジは、仕様がどこまでテストされたのか？に対してVDMToolsが提供する1つの指標です。VDMToolsでは、インタプリタで実行した仕様の場所や実行カバー率を計測（VDMToolsで計測しているテストカバレッジはC0レベルです）していますので、その仕様がどこまでテストされたかを簡単に見ることができます。このテストカバレッジを1つの指標として、テストカバレッジ100％を目指すことで、仕様自身の正当性確認がどの程度されているかが見えます。もちろん、テストカバレッジが100％になったからといって、仕様の正当性確認が完全になったわけではありませんが、この指標を達成し、必要と判断した場合はさらにテストケースを追加することで仕様の品質は高まっていきます。

　テスティングフレームワークは、テスト環境を容易に構築できるフレームワークです。VDM++には、JavaのJUnitのようなユニットテストの仕組みを提供するフレームワーク「VDMUnit」があります。このフレームワークを採用することで、テスト実行については特に考える必要がなく、VDM仕様に対してのシナリオを記述するだけで簡単にテスト実行が可能になります。このシナリオを要求やユースケースをベースに記述することで、仕様が要求に対して妥当性があるかを確認できます。なお、VDMUnitはVDM++の教科書である「Validated Designs for Object-oriented Systems」のサンプルページからダウンロードできますので、ぜひ試してみてください（注）。

※注：Validated Designs for Object-oriented Systemsのサンプルページにある「chapter9.zip」の中に、ほかのサンプルと一緒にVDMUnitが入っています。

　そして、記述したテストケースはVDMToolsのインタプリタで繰り返しテストをすることが可能です。仕様を定義する際、頻繁に仕様の追加や変更が発生しますが、回帰テストをすることで、それらの追加や変更を加えたことによって、もともと定義していた仕様に対して影響があるかどうかを検証できます。つまり、常に仕様追加・変更の前後で影響が発生しないことを確認しながら開発を進めることができるということです。

分かりやすく仕様を記述する

　筆者はこれまで社内外の仕様書をいくつか見てきました。それらのほとんどが日本語で記述されており、またほとんどに共通する問題点として、用語定義の統一がなされていないことが挙げられます。同じような用語が少しずつ違った用語として、仕様書のいろいろな場所に散りばめられているのです。この用語定義のわずかな違いに対する解釈の違いが、最終的にソフトウェアのバグとして顕在化することが往々にしてあります（このような経験をお持ちの方も多いのではないでしょうか？）。

　一方、VDMは明確な構文定義のうえで成り立っているため、上記のような用語統一がされないということはありません。しかしその半面、記述が一見プログラムのように見えてしまうため、VDMの記述方式に決まり事を作らずに個々人が自分のルールで記述してしまうと、統一感がなく、分かりづらい記述になってしまう可能性があります。

　これらの問題点への対策は、VDMのコーディング規約を作ることです。読者の皆さんがプログラムを記述する際にも、プロジェクト内や社内でコーディング規約を決め、運用していると思います。ここで紹介するコーディング規約もプログラムに対するコーディング規約と大きくは変わりません。ただ、プログラムに対する通常のコーディング規約は主に命名規則や段付けなどを定義しますが、VDMは仕様であり、その「意味」を重んじますので、今回は命名規則だけでなく、「意味」に対する規約も説明します。

仕様の「意味」と用語定義の統一を実現する

　まず、仕様の「意味」に対するコーディング規約は、「VDMの言語が持つ組み込み型（int、nat、real、charなど）をあまり使わない」ということです。例えば、連載第1回で記述した仕様の中に、「年齢」という自然数（VDM++の組み込み型でいえばnat）で表現する型を定義しました。

　なぜあえて自然数で表現できるものを「年齢」型として定義したのでしょうか？これはVDMが記述しているのがプログラムではなく、「仕様」であるためです。仕様の大きな役割として、「下流工程への間違いない伝達」があります。このためには、単に正確に記述されているだけでは足りず、読みやすく分かりやすい記述である必要があります。

　そのため、自然数であるから型を定義せずに“nat”としてしまうのではなく、明示的にその要素が何を表すのか？を表現するために「年齢」という型を定義しているのです。また、このように明示的な定義を行うことは、同時に「年齢」という用語の定義をしているともいえます。これらを集めることで用語辞書を作ることができるという効果もあります。

VDMにおける命名規則

　VDMにおける命名規則の一例を表2に示します。VDMはプログラムと違い日本語が使えますので、日本語が使えるからこその命名規則作りをお勧めします。



クラス名、型名	「クラス名」「型名」（クラスや型の名前にカギ括弧を付けて表現）
インスタンス変数	i インスタンス変数（変数名にインスタンス（instance）の頭文字「i」を付けて表現）
引数	a 引数（引数名に引数（argument）の頭文字「a」を付けて表現）
値取得関数	～を得る（いわゆるget関数はこのように表現）
真偽判定関数	～か？（true／falseを返すような関数はこのように表現）
表2　VDMにおける命名規則の一例