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

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

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

クラス図から陰仕様を記述する

　VDMでは仕様記述を「陰仕様」から「陽仕様」へと段階的に詳細化していくと第1回「ライトウェイトな形式手法で高品質な仕様をこの手に！」で説明しました。ここでは陰仕様を記述します。

　陰仕様はクラスや型、インスタンス変数といった仕様の構造と、定義した関数や操作が持つ機能の概要を表現します。具体的に陰仕様に記述される要素とVDMでの表現は、表1のとおりです。

要素	クラス図	VDM
クラス	クラス	クラス
クラス内変数	属性	インスタンス変数
固定値	ReadOnlyプロパティ属性	定数
機能名	操作名	関数・操作名
入力	操作の引数	引数の型と仮引数名
出力	操作の戻り値	戻り値の型
制約条件	ノート or OCL or タグ付き値	事前・事後条件
表1　クラス図とVDMにおける要素のマッピング

　これらは、その機能がどのような条件のときに何をすべきか？ を示しているといえます。つまり、陰仕様は“What”と“How”の関係でいうところの“What”を表すものです。

　それでは、実際の陰仕様を見ていきましょう。

　前回、仕様の構造をクラス図に定義しましたので、まずはクラス図からVDMの陰仕様を記述します。図1にVDMの陰仕様を記述する際の材料となるクラス図を示します。

図1　クラス図

　2008年11月19日に公開された「VDMTools 8.2b」では、UMLモデリングツールとVDMToolsのツールチェーンを実現する「UMLリンク」という機能が追加されています。この機能が追加される前は、前回記述したようなクラス図から陰仕様を手動で記述していました。本来、クラス図にモデル要素がしっかり書かれていれば、陰仕様を記述するのは機械的な作業です。そのため、今回の例はUMLリンクを使って、陰仕様を自動生成しました。このUMLリンクは、UMLモデリングツールである、Enterprise ArchitectやJUDE/Professionalとモデルの相互変換をする機能で、現段階ではクラス図とVDM++の相互変換を実現しています。UMLリンク機能の使い方は、VDM公式Webサイトに掲載されていますので、そちらを参照してください。

　ここでは陰仕様の一例として、「ライン監視制御」クラスのVDM記述を見てみましょう。

 1 :  class ライン監視制御
 2 :  
 3 :  instance variables
 4 :    private iライン状態 : ライン状態;
 5 :    private i光センサー : 光センサー;
 6 :  
 7 :  operations
 8 :    public ライン状態を判定する : () ==> ライン状態
 9 :    ライン状態を判定する() ==
10 :      is not yet specified
11 :    pre
12 :      i光センサー.黒線レベル値を読み取る() <> nil
13 :    post
14 :      cases mk_(i光センサー.黒線レベル値を読み取る(), RESULT):
15 :        mk_(<黒閾値以下>, <黒>) -> true,
16 :        mk_(<白閾値以上>, <白>) -> true,
17 :        mk_(-, <不明>) -> true,
18 :        others -> false
19 :      end;
20 :  
21 :  end ライン監視制御 

　1〜5行目は、仕様の構造としてクラスとインスタンス変数が定義されているのが分かります。ただこの陰仕様は、VDMToolsで自動生成された陰仕様ですので、型が生成されません。これはクラス図に型を定義できないためで、このままではインスタンス変数で指定している型（ライン状態）が定義されていないため、整合性が取れない記述になってしまいます。この解決方法については、次節の「陰仕様を洗練させる」で説明します。

　7〜19行目では操作の陰仕様定義をしています。今回は「ライン状態を判定する」という操作を定義しています。8行目を見ると、入力としては何ももらわず、出力としてライン状態型を戻すことが分かります。そして10行目にはこの操作の本体として、「is not yet specified」と書かれています。これはVDMの予約語で、陰仕様段階では仕様の詳細な実現方法（アルゴリズム）には言及せず、まずは関数や操作の入出力と制約条件を明確にする、つまり仕様を段階的に詳細化するための手法です。

　11〜12行目では、この操作の制約条件として事前条件が書かれています。事前条件は「pre」で始まり、それ以降を論理式の形で記述します。今回は光センサーの読み取る黒線レベル値がnil（何も値が取得されていない）でない、つまり初期状態ではなく、何らかの値を読み取れることが定義されています。

　13〜19行目では、この操作の事後条件が書かれています。事後条件は「post」で始まり、事前条件と同じく論理式の形で記述します。今回の例では、読み取った黒線レベル値と戻り値の関係が事後条件で表現されています。具体的には、黒線レベル値が「黒閾値以下」であれば戻り値が「黒」、黒線レベル値が「白閾値以上」であれば戻り値が「白」、それ以外であれば戻り値が「不明」であることを表しています。

　ここまででまずは陰仕様の土台が完成です。次は、陰仕様を洗練させて、完成させましょう。

陰仕様を洗練させる

　UMLリンクで自動生成された陰仕様は、型が定義されず整合性の取れない記述のままであると前述しました。ここでは型定義を追加することで、陰仕様を完成させます。なお、VDMToolsのUMLリンク機能を使わない場合のこの作業は、クラス図から陰仕様を手で記述する際に同時に行います。

　まずは型定義をします。型として取り扱いたい要素を、クラス図ではクラスとして存在させ、型であることが分かるような表現をしました。これをどのクラスに定義すべきかを決め、そのクラスに型として定義します。

　例として、前節でも用いた「ライン監視制御」クラスに関する型を定義してみます。下記の例では、「黒」と「白」の値を取る「ライン状態」型を定義しています。

types
  public ライン状態 = <黒> | <白>; 

　これでライン監視制御クラスの整合性が取れるようになりました。ほかのクラスに関連する型も同時に定義をすることで、整合性の取れた陰仕様が完成します。

陰仕様の静的チェックをする

　ここまでの作業で、VDMの陰仕様が完成しましたので、VDMToolsを用いて静的チェックを行います。なお、静的チェックは今回の説明の都合上、陰仕様が完成してから行っていますが、陰仕様を記述している途中で随時静的チェックをすることをお勧めします。その際は、記述途中であることが原因のチェックエラーと、記述自体が原因のチェックエラーを見極めながら記述をしてください。

　VDMToolsを用いた静的チェックは、3種類の方法があります。1つ目は「構文チェック」です。これは、記述した仕様がVDMの構文どおりに書かれているかどうかをチェックするものです。

　2つ目は「型チェック」です。これは、記述全体の中でクラスや型の整合性をチェックするものです。例えば、定義されていない型を関数の入力に用いていたり、参照できるはずのない型やインスタンス変数を参照するような事前・事後条件を記述した場合にエラーとなります。

　3つ目は「証明課題生成」です。これは、VDM記述の中から証明すべき課題を自動的に生成するVDMToolsが持つ機能です。この機能で生成された証明課題をすべて証明することで、数学的に仕様を証明できます。こちらの機能は今回の連載では説明しません。ご興味がありましたら、まずは記述したVDMから証明課題を生成してみてください。