VDMはソフトウェア開発でこう使う！：誰でも使える形式手法（2）（2/3 ページ）

“VDMを開発プロセスの中でどのように活用すべきか”について、「導入」と「運用」に分けて、具体的な施策を示しながら解説する。

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

VDMをどのように記述していくか？

　ここでは、VDMで仕様を記述するときに、どのように記述していくのか？ という“VDMの記述プロセス”について紹介します。

VDM単体での記述プロセス

　VDM単体で仕様記述を進めるプロセスを図2に、その手順を以下に示します。

1. 要求を読む
2. 要求から状態を分析し、インスタンス変数を抽出する
3. 主に名詞からクラスと型、主に動詞から関数と操作を抽出する
4. クラスと型とインスタンス変数を定義する
5. 関数と操作の名称、入出力（シグネチャ）を定義する
6. 要求からシステム中で常に成立すべき不変的性質を、型やインスタンス変数の不変条件として定義する
7. 要求から機能に関する事前・事後の制約条件を、関数・操作の事前・事後条件として定義する
8. 構文チェック、型チェックをし、仕様の静的チェックをする（静的チェックはこの工程に限定するのではなく、モデル作成中随時実施する）　
   →ここまでが「陰仕様定義」
9. 関数・操作の中身を定義していく　
   →ここまでが「陽仕様定義」
10. 要求、VDM記述からシナリオを検討し、テストケースとしてVDM仕様を記述する
11. 仕様を実行し、仕様の動的チェックをする

図2　VDM単体で仕様記述を進めるプロセス

　この記述プロセスをはじめVDMでは、陰仕様から陽仕様へと仕様を段階的に詳細化していきます。VDMにおける関数・操作は、システムにおける1つ1つの機能を表現しているといえます。つまり、陰仕様では機能の入出力と制約条件を明らかにすればよく、その機能の詳細は陽仕様で記述します。ソフトウェア開発において、仕様を定義・記述するような段階で仕様がすべて決定していることはまれだと思います。そこで、仕様を段階的に詳細化することで、仕様における「抜け」「モレ」を排除しながら徐々に仕様を決定できます。これが、この記述プロセスでのメリットになります。

　反対にこの記述プロセスでのデメリットは、VDMのみで仕様記述を進めて行く点にあります。VDMに慣れている場合はモデルを考え、そのモデルをVDM単体で記述していくことも十分可能ですが、VDMはテキスト形式であるため、UML（Unified Modeling Language）などの図式表現に比べて考えを整理しづらいという点に難があります。また、モデルがテキスト形式のVDMでしか残っていないことは、モデルの可視性や他者とのコミュニケーションに問題を抱えることになります。

　そこで、次に紹介する『UML＋VDM』による仕様記述が有効になります。UMLは現場においてよく使われていますし、UMLの図が持つ可視性はモデリングをするうえで大きな効果をもたらします。VDMとUMLとを組み合わせて使うことは、現場にVDMを効果的に導入するのに適しているといえます。

UML＋VDM

　VDMとUMLを融合させて仕様を記述する際のプロセスを図3に、その手順を以下に示します。

図3　VDM＋UMLで仕様記述を進めるプロセス

1. 要求を読む
2. 要求からユースケースを検討し、ユースケース記述で表現する
3. 仕様における振る舞いを分析し、状態遷移図やアクティビティ図で定義する
4. 仕様の構造と機能の概略を分析し、クラス図で定義する
5. クラス図を参考にVDM陰仕様を定義する
6. 構文チェック、型チェックをし、仕様の静的チェックをする（静的チェックはこの工程に限定するのではなく、モデル作成中随時実施する）
7. VDM陰仕様と状態遷移図、アクティビティ図からVDM陽仕様を定義する
8. ユースケース記述、VDM陽仕様からシナリオを検討し、テストケースとしてVDMを記述する
9. 仕様を実行し、仕様の動的チェックをする

　この記述プロセスでは、まずUMLを用いて仕様の概要を描き、それを基にVDMで詳細を記述します。この記述プロセスは一連の流れを通して行ったら“これで完了”というものではなく、UML・VDMのそれぞれのモデルに変更があれば、その変更を双方で対応する要素（表1）に反映しながらモデルを成長させていきます。ここで注意すべきなのは、“UMLとVDMとの間に違いがあった場合、常にVDMが正になるように運用すること”です。

　また、UMLをともに用いた場合のモデリングは、上記の手順にあるUMLの各図を記述する前に実施する必要があります。ちなみに、その際のモデリング方法はVDM単体記述プロセスの手順2〜5と変わりません。

	UML	VDM
	クラス	クラス
	属性（特に状態）	インスタンス変数
	操作	操作、関数
表1　UML・VDMで対応する要素

　UMLをともに使うことで得られるメリットは、UMLという現在のソフトウェア開発で広く使われている手法の知識を生かせる点にあります。すでに持っている知識を使うことは、モデルを考えやすくできますし、手法導入のしやすさを促進できます。また、VDMを知らないメンバーや顧客とコミュニケーションを取る際に、相手がUMLを知っていればUMLをベースにコミュニケーションを取ることができます。開発において、コミュニケーションの円滑化はとても重要な要素ですので、これも大きなメリットといえます。

　反対にこの記述プロセスでの注意点は、あまりUMLでの記述に捕われていない点にあります。UMLの後にVDMで記述することを考えると、実はUMLで表現できることはわずかです。また、UMLで記述したモデルは検証ができないため、UML記述の完全さを求めることは本質ではありません。そのため、UMLとVDMをともに使う場合は、UMLが持つ“可視性”とVDMが持つ“厳密性”を生かした（意識した）モデル作りが成功のカギとなります。

仕様を構造化する

　VDMが持つ言語自体は、表現力が豊かな分、複雑でもあります。そのため、しっかりとモデリングをせずに記述してしまうと、分かりづらく再利用性に優れない仕様が出来上がってしまいます。また、記述者それぞれが違うモデリングをしてしまうと、記述のレベルがバラバラになり、せっかく記述した仕様が無意味になってしまいます。

　これを防ぐためには、しっかりと仕様を構造化し、記述者によって詳細度や記述方式に違いが出ないようにすること、つまり“仕様のフレームワーク”を考えることが重要となります。このフレームワーク分けは、例えば以下のような観点で行います。

• 機能仕様の記述をしやすくするための構造にする
• 仕様のテスト実行を行いやすくするための構造にする
• 仕様記述者の役割分担に応じた構造にする
• 仕様の部品化を促進し、再利用しやすい構造にする

　こうしたフレームワークの採用により得られるメリットが2つあります。

　1つは、仕様記述メンバーのスキル分散と責務分担ができる点です。仕様を記述するメンバー全員がVDMに精通し、自由自在に操ることができるというのが理想ですが、これには習得コストが掛かります。そこで、図4のように、VDMに精通した少数精鋭のコアメンバーチームを作り、そのメンバーに上記のような観点を考慮したフレームワークを作ってもらいます。そうすることにより、残りの仕様記述メンバーはフレームワークにのっとった形で仕様を記述できますので、仕様自体を記述することに集中でき、VDM自体のスキルはそんなに高くなくても記述が可能になります。

図4　仕様記述メンバーのスキル分散と責務分担

　また、近年の開発では新規に一から作り上げるより、派生開発で既存製品の仕様に追加・修正することが多くあります。2つ目のメリットは、そんな派生開発において威力を発揮するもので、フレームワークを部品化と再利用性を考慮した構造にすることで、いろいろな製品に使える共通部分を仕様部品として再利用できるという点にあります。VDMで記述された仕様を再利用することは、すなわち“仕様として検証済みである部品”を使える、ということです。この部品を蓄積していき、ライブラリとしてまとめておくことにより、派生開発の新規仕様部分の仕様記述に集中できますし、生産性を高めることができます。