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

今回は、「LEGO Mindstorms NXT」のライントレース仕様をテーマに記述したUMLを基に、VDMによる仕様記述の手順を詳しく解説する！

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

　前回「VDMを用いた仕様記述・検証 〜 モデリング編 〜」では、レゴ社のLEGO Mindstorms NXT（以下、Mindstorms）のライントレース仕様をテーマに要求を分析し、UMLでモデルを記述しました。

　今回は、前回記述したUMLを基にVDM記述をしていきます。ここからは、VDMの構文がいくつか出てきますので、VDM information web siteのVDMToolsマニュアルに掲載されている「VDM++ 言語マニュアル」をダウンロードし、必要に応じて参照しながら読み進めてください。

	関連リンク：
⇒	VDM information web site

なぜモデルをVDMで記述するのか？

　読者の中には、「前回UMLで要求をモデル化したのだから、あえてVDMで記述する必要はないのではないか？」と感じている方もいらっしゃるかもしれません。そこで、“なぜVDMを記述するのか”について説明することから始めたいと思います。

　仕様をUMLで記述するにせよ、日本語で記述するにせよ、問題となるのは以下の2点です。

• 仕様記述者の意図が正確に仕様の読み手へ伝わらない
• 記述した仕様の正しさが分からない

　1点目の「仕様記述者の意図が正確に仕様の読み手へ伝わらない」のは、記述があいまいで一貫性がなく記述されているために、さまざまな解釈ができてしまうことが原因です。UMLのような図式表現ではある程度緩和されますが、日本語での仕様表現ではあいまいさが顕著に表れます。これでは「仕様を正確に他者に伝える」という役割を果たすことができません。また、仕様中に表れる用語の定義が一意でないため、さらに仕様の読み手を混乱させるのです。

　2点目の「記述した仕様の正しさが分からない」のは、仕様に対する検証基準が明確でないことと、仕様自体の制約条件が明確でないことが原因です。一般的に仕様の検証方法といえば、仕様をレビューすることです。しかし、レビューでは明確な検証基準がなく、検証品質はレビューアの力量に左右されることが往々にしてあります。また、仕様自体の制約条件を明確にしていないために、1つ1つの機能が持つ責務やその機能を使う側に課せられる責務が分からず、それがテスト工程でバグとして顕在化するのです。

　上記のような問題を解決するには、一貫性のある仕様を制約条件も含めてあいまいさなく記述し、明確な検証基準の下、人手に頼らない検証が必要です。これを実現するための1つの方法が、今回紹介するVDMでの記述と検証になるのです。

　早速、MindstormsのVDM記述を解説したいところですが、まずはVDM記述の全体構成を説明します。

VDMの全体構成

　本連載で取り扱っているVDM++は、以下のように構成されています。

class クラス名
  types
    型定義
  values
    定数定義
  instance variables
    インスタンス変数定義
  functions
    関数定義
  operations
    操作定義
end クラス名 

　ほかにも、「sync」や「thread」を使うことで同期制約やスレッド定義を記述できます。ここでは、主に使われる上記定義について簡単に説明します。

　VDM++の最も大きな記述単位はクラスです。そして、クラスの中に「types」や「functions」のようなキーワード別にそれぞれの要素を定義していきます。それぞれの要素を記述する文法は別途VDM++ 言語マニュアルを参照してください。これらの要素を記述する順番は関係がなく、typesが2個所出てくるような重複も許されています。

　それではMindstormsを例に、VDMを記述していく過程を見ていきましょう。