ライトウェイトな形式手法で高品質な仕様をこの手に！：誰でも使える形式手法（1）（3/3 ページ）

仕様の“不確かさ”が原因で痛い目を見た。そんな経験をお持ちの皆さん、この機会に形式手法をマスターし、高品質な仕様を作成してみませんか。

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

VDMを用いた開発を支援する「VDMTools」とは？

　VDMを用いた開発を支援するツール「VDMTools」はデンマークの政府資金で開発されたツールで、現在CSKが開発・提供を行っています。

　VDMToolsの機能を図2に示します。

　主な機能として、「構文＆型チェッカー」「インタプリタ」「コードカバレッジ」「ドキュメント生成」などが挙げられます。これらの機能により、記述したVDMの静的チェックから動的チェック、カバレッジ測定、ドキュメントの生成が可能となります。対応するプラットフォームはWindows、Mac OS X、Linuxで、日本語化もされています。

図2　VDMToolsの機能
※各種UMLモデリングツールとXMIインターフェイスにて対応予定

　VDMToolsの機能についてはVDM公式サイトで詳しく紹介されていますので、興味のある方はそちらを参考にしてください。また、会員登録さえすればVDMToolsの一部機能を限定したバージョン「VDMTools Lite（画面1）」を無料でダウンロードできますので、気軽に試してみるのもよいでしょう。分からないことはVDM公式サイトを通して質問してみてください。

画面1　VDMTools VDM++ Toolbox Liteの画面

	関連リンク：
⇒	VDM公式サイト

VDMで仕様を記述する

　さて、ここからはVDMの中で主に使用されている仕様記述言語である「VDM++」を使って具体的にどのような記述を行うのかを簡単な例題を用いて紹介します（まずは、雰囲気をつかんでください）。

　この例題は、「名前」と「年齢」だけを登録するとてもシンプルな“会員登録機能”です。以下の「日本語仕様」と「VDM仕様」を見比べてみてください。いかがですか？ 何となく日本語仕様（自然言語による仕様）の“不確かさ”が伝わってきませんか？

日本語仕様

VDM仕様

 1 : class 『会員登録』
 2 : types
 3 :   public 「名前」 = seq of char;
 4 :   public 「年齢」 = nat;
 5 :   public 「会員」 :: 名前 : 「名前」
 6 :                      年齢 : 「年齢」;
 7 : 
 8 : instance variables
 9 :   i会員集合 : set of 「会員」 := {};
10 : 
11 : operations
12 :   public 新規会員登録 : 「会員」 ==> ()
13 :   新規会員登録(a会員) ==
14 :     i会員集合 := i会員集合 union {a会員}
15 :   pre
16 :     len a会員.名前 > 0 and
17 :     a会員.名前 not in set { x.名前 | x in set i会員集合 }
18 :   post
19 :     i会員集合 \ {a会員} = i会員集合~ and
20 :     card i会員集合 = card i会員集合~ + 1;
21 : end 『会員登録』 

　それでは、VDM++による記述内容を上から見ていきましょう。

　VDM++はオブジェクト指向言語ですので、クラスを軸として記述を行っていきます。1行目で、“『会員登録』”というクラスを定義しています。このように、すべての識別子に日本語を使うことができます。

　2行目の“types”部分は、型定義です。今回は3つの型を定義しました。1つ目は“「名前」”型です。これは文字の列、すなわち文字列を表しています。2つ目は“「年齢」”型です。これは自然数で表現しています。3つ目は“「会員」”型です。これはVDM++のレコード型を使っています。レコード型はC言語でいうところの構造体です。会員は情報として名前と年齢を登録しますので、レコード型でまとめて表現をしました。

　8行目の“instance variables”部分は、インスタンス変数定義です。これはJavaでいうところのメンバ変数に相当し、クラス内で動的に変化するデータや状態を定義します。今回は“set of 「会員」”（「会員」型の集合）を“i会員集合”として定義しています。

　11行目の“operations”部分は、操作定義です。VDMでは関数と操作を用いて、機能を表現します。これらの違いについては、コラム（文末）をご覧ください。今回は“新規会員登録”という操作を定義しており、引数として“「会員」”型のデータを取ります。操作内で行う処理は、インスタンス変数である“i会員集合”へ引数である“a会員”を追加するのみです。

　この例は、振る舞いは非常に単純ですが、事前条件と事後条件をそれぞれ2つずつ定義しています。15行目の“pre”は事前条件を記述するブロックで、18行目の“post”は事後条件を記述するブロックです。ここでは詳細な構文の説明は割愛しますが、おのおの表現しているのは以下の条件です。

• 事前条件1（16行目）：登録しようとしている会員の名前が入力されていること
• 事前条件2（17行目）：登録しようとしている会員の名前が登録済みでないこと

　

• 事後条件1（19行目）：会員登録処理後の登録済み会員から登録した会員を除くと、処理前の登録済み会員と同一であること
• 事後条件2（20行目）：登録処理後の会員数は、処理前の会員数より1人分増えていること

　ここでは、ごく簡単にVDM++のイメージを持っていただくために一部の構文を解説しました。より詳細な構文の説明は、VDM公式サイトに言語マニュアルやオンラインマニュアルがありますので、そちらを参照してください。

コラム　関数と操作の違い

今回の例題では「操作」を用いました。VDMでは関数と操作を明確に分けて記述を行いますが、一般的なプログラミング言語では操作を関数として統合する場合がほとんどです。では、両者の違いはどこにあるのでしょうか？

それは、操作はインスタンス変数（Javaでいうところのメンバ変数）にアクセスし、値を書き換えることもできますが、一方の関数はインスタンス変数にアクセスすることができず、入力パラメータから戻り値を導き出すという点です。このような性質から、操作に比べて関数は安全性が高いといえます。なぜなら、関数は刻々と状態の変化するインスタンス変数の影響を受けず、入力パラメータに対して事前条件や関数内部での制約を与えるだけでよいからです。

VDMで仕様を記述する際は、この関数と操作をうまく使い分けることにより、安全性と自由度を兼ね備えた仕様を構築できます。

---

　今回は、「形式手法」「VDM」について紹介しました。形式手法は“不確か”な仕様を“厳密”にする手法だということをお分かりいただけたと思います。次回からは、VDMを用いてどのように仕様記述・検証を行うのか？ を例題を交えて詳しく解説していきます。お楽しみに！（次回に続く）

【参考文献】

（1）「形式手法の技術講座―ソフトウェアトラブルを予防する」 佐原 伸／ソフトリサーチセンター

（2）「ソフトウェア工学の基礎」 玉井 哲雄／岩波書店

（3）「ソフトウェア工学の道具としての形式手法 −彷徨える形式手法−」 中島 震