VDMを用いた仕様記述・検証 〜 仕様記述編 〜：誰でも使える形式手法（4）（3/3 ページ）
今回は、「LEGO Mindstorms NXT」のライントレース仕様をテーマに記述したUMLを基に、VDMによる仕様記述の手順を詳しく解説する！
陽仕様を記述する
陰仕様の記述、静的チェックが終わると、次は陽仕様の記述に移ります。陽仕様では、陰仕様で定義した入力と事前条件を基に、どのように事後条件にあった出力を求めるか？ のアルゴリズムを記述します。つまり、陽仕様は“What”と“How”の関係でいうところの“How”を表すものです。入力や出力がない場合も、陰仕様において制約条件にその関数や操作に求められる責務を記述しますので、そのアルゴリズムを記述していきます。
例として、引き続き「ライン監視制御」クラスを題材に、「ライン状態を判定する」操作の陽仕様を記述していきます。
1 : class 「ライン監視制御」 2 : 3 : types 4 : public 「ライン状態」 = <黒> | <白> | <不明>; 5 : 6 : instance variables 7 : private iライン状態 : 「ライン状態」; 8 : private i光センサー : 「光センサー」; 9 : 10 : operations 11 : public ライン状態を判定する : () ==> 「ライン状態」 12 : ライン状態を判定する() == 13 : cases i光センサー.黒線レベル値を読み取る(): 14 : <黒閾値以下> -> return <黒>, 15 : <白閾値以上> -> return <白>, 16 : others -> return <不明> 17 : end 18 : pre 19 : i光センサー.黒線レベル値を読み取る() <> nil 20 : post 21 : cases mk_(i光センサー.黒線レベル値を読み取る(), RESULT): 22 : mk_(<黒閾値以下>, <黒>) -> true, 23 : mk_(<白閾値以上>, <白>) -> true, 24 : mk_(-, <不明>) -> true, 25 : others -> false 26 : end; 27 : 28 : end 「ライン監視制御」
陰仕様からの変化は、13〜17行目に表れています。陰仕様ではこの部分は「is not yet specified」とし、定義をしていませんでしたが、陽仕様はこの部分でどのように「ライン状態を判定する」のかを記述しています。
前回のとおり、今回は仕様段階で黒線レベル値を抽象化したので、これにのっとった判定方法にしています。具体的には、読み取った黒線レベル値が「黒線閾値以下」であれば「黒」（14行目）、「白線閾値以上」であれば「白」（15行目）と判定しています。また、ここではVDM++のcases文を用いてその判定方法を表現しており、上記判定基準以外（others部分）であれば「不明」と判定することとします。
ここまでで、一通りのVDMによる仕様記述は終了です。誌面の都合上すべてのVDM仕様を掲載できませんが、UMLでモデルを記述していたときに比べ、さまざまな変更がVDMではなされています。これらの変更は、VDMを記述していく過程で発見したり、静的チェックによって発見したりすることによって行われています。図2にVDM記述後のUMLクラス図を掲載します。クラス構成は変化していませんが、おのおののクラスに定義した属性や操作に違いがあります。
例えば、モータークラスの「回転する」操作では事前条件を定義していませんでしたが、図3のようにVDM記述をしていくうちに停止するときの回転速度と同じ速度を与えてはいけないことを追加しています。
この部分のVDM記述は、以下のようになります。
pre a回転速度 <> mk_token(0)
また、単純な間違いとして前回のクラス図には「ライン状態を判定する」という操作が「ライン監視制御」クラスと「光センサー」クラスの両方に定義されていました。これは両方にある操作ではなく、「ライン監視制御」クラスにのみあるべき操作ですので、図4のようにVDM記述では削除しています。
ほかにも属性の保持方法や各クラスの持つ状態をどのように取得するかなどが抜けていましたので、そちらも追加しています。UMLでは正しいと思って記述していてもVDMを使うことで、さまざまな間違いを発見できます。これらの間違いに多い傾向として、UML上での抜け・モレ・重複があります。これはやはりクラス図自体がレビュー以外の検証手段を持たないことが大きな原因となっているといえるでしょう。
陽仕様の静的チェックをする
陰仕様の記述時にも静的チェックをしました。当然、陽仕様記述時にも静的チェックは必要です。特に陽仕様はアルゴリズムを記述していく分、ほかのクラスとの関連が多くなったり、属性や操作内の整合性を取ったりするため、型チェックエラーが数多く出ることがあります。
そこで、陽仕様記述時もこまめに静的チェックをすることをお勧めします。もし陽仕様をすべて記述してから静的チェックをすると、膨大な数のエラーが出て、どこから修正したらよいか分からなくなることもあります。その際は、VDMToolsのエラーウィンドウに出ているエラーを上から解決するようにしてみてください。上から解決していくと、1つのエラーから芋づる式にエラーになっている部分を効率的に修正できます。
今回は、前回記述したUMLをベースにVDMを記述する過程を説明しました。ご覧いただいたように、VDM記述自体はあまり難しくありません。
以下にここまで記述したVDMのコードを掲載しておきます。まだ、VDMToolsによる静的チェックのみで、次回実施する予定の動的検証をしていませんので、仕様バグが含まれているかもしれませんが参考にしてください。なお、仕様バグを含まず、テストケースも含んだ仕様全体は次回に公開します。
次回はいよいよ最終回となります。今回記述したVDMを検証する過程を解説します。「VDMを使うことで仕様が検証できる」。これはVDMの大きな特長であり、大きな目的でもあります。ご期待ください！（次回に続く）
Copyright © ITmedia, Inc. All Rights Reserved.
いまさら聞けない 形式手法入門