ディペンダブル・システムのための形式手法の実践ポータル

このページでは，形式手法・ツールの考え方，多様性を説明するための例として，VDMという手法とその代表的ツールであるVDM++ Toolboxについてごく簡単に説明します．VDMは仕様を形式化する手法であり，フェリカネットワークスが活用したことで日本でよく知られるようになりました．VDMについての詳細は解説ページに別途まとめます．

VDM概要

VDMは「形式仕様記述」と呼ばれる手法の代表的なツールです．形式仕様記述は，システム状態のデータ構造やそれを操作するメソッドの機能等に関する仕様を明示化，検証する手法です（形式化の対象による分類です）．検証する性質としては，「あるメソッドが適切な条件の下呼ばれていれば，期待された結果が必ず起こるか」「メソッドの実行によって不具合のある状態に到達することはないか」といった各メソッドの実行の効果に関する性質を考えます．

簡単な例題

例題として，イベントの参加登録者を管理するシステムを考えてみます．簡単のためイベントは１つしか考えないことにして，このシステムでは．「そのイベントへの登録者一覧」と「そのイベントの定員」を管理しているとします．このシステムに対する操作としては，ユーザのイベントへの参加登録やその取り消しが考えられます．

システムが保持する情報には「常に満たすべき性質」が存在することが多々あります．今回の例の場合，「イベントの参加登録者はイベントの定員以下である」という性質が常に成り立つべきと考えられます．このようにシステムの状態において常に成り立つべき性質のことを不変条件といいます．VDM（手法の名前）におけるオブジェクト指向言語VDM++を用いた場合，次のようにこのような仕様を記述することができます．

class RegistrationManager
    instance variables
        private capacity: nat;
        private registered: set of User;
        inv card registered <= capacity;

この記述ではRegistrationManager というクラスを宣言し，２つのインスタンス変数を定義しています．１つは定員を表す capability （定員）という変数で，その型は nat （自然数）となっています．もう１つは参加登録済みの人の集合を表す registered という変数で，その型は User の集合となっています（Userクラスは別途定義されているとします）．ここで上記の不変条件は，inv（不変条件，invariant）から始まる行において記述されています．この不変条件では，集合 registered の要素数（card，cardinarityの意）が capability 以下であることを宣言しています．

加えて，このシステムに対する操作の１つとして，「参加登録を受け付ける」という操作を考えてみます．ここで上の不変条件を考えると，この操作は「参加登録が定員に達していない」ときのみ有効に実行されるべきと考えられます．このように操作（メソッド）の期待される実行のための前提・想定のことをその操作の事前条件といいます．VDM++において上記の操作は以下のように宣言できます．

public register: User ==> ()
register(p) ==
   registered := registered union {p}
pre card registered < capability;

文法について詳しいことは述べませんが，１行目では register という操作が Person を引数として受け取り戻り値がない（ () は void に相当）ことを宣言しています．２，３行目では register の本体を宣言しています．ここではインスタンス変数 registered に p を加えて更新しています（ union は集合の和を表す演算子）．４行目では，上で述べた事前条件， registered の要素数（card）が capability 未満であることを宣言しています．

このようにVDMでは，不変条件や事前条件を明示しながらクラス（モジュール）構成やデータ型，メソッド等の仕様を記述します．ここで検証する性質としては，「事前条件が成り立たないような操作の呼び出しを行っていないか」「事前条件が成立する状況で操作が実行された際に，不変条件が崩れることがないか」といったこととなります．

VDM手法の代表的なツールとして知られているVDM Toolboxでは，手軽な検証手法として形式仕様の実行による検証を支援しています．カバレッジを計測しながらテスティングを行うことにより，一般的な開発者が慣れ親しんでいる方法で仕様を検証します．その際には不変条件や操作の事前条件を監視し，成り立たない場合を洗い出すようにします．不変条件や事前条件に関連して証明すべき課題を列挙させることもできるので，より信頼性が求められるシステムの場合，人手によりチェック（証明）をしていくことも考えられます．

VDMではこのように仕様を曖昧さのない形で厳密に明示化します．その過程において，特に日本語表現による曖昧さや不正確さを洗い出すことができます．仕様に対する誤解や思い込み等は，統合テスト時など後で発覚するほど手戻りのコストが大きいため，VDMでは開発の早期における仕様の明確化を考えています．特にその際，実装の詳細を明示せず，システムの状態や個々の操作がどのような条件を満たすべきかを明示化します．操作の追加時や操作呼び出しの追加時等に不変条件や事前条件が見落とされるとバグの原因となるため，これらを洗い出し，厳密に記述し，共有や検証を行うことは非常に有効です．

例題補足

上の問題は非常に簡単な例であり，操作において実行可能な動作本体（この場合代入文）を書いています．しかし仕様としては，「操作をどう実現するか」よりも「操作が何をするか」を明示すべきです．つまり，「グローバル変数やインスタンス変数をどう変化させるのか」，「出力はどういう条件を満たすのか」，といった実行の効果に関する記述です．VDMにおいてはそのような操作の効果を操作の事後条件といいます．例えばソート処理の場合，「入力として受け取ったリストが小さい順に並んだものが出力である」ということが事後条件となるでしょう．

操作の事前条件・事後条件だけ定めればその操作の意図は明確に定まるので，それで十分かもしれません．開発の初期段階では「どうソートを実現するか」までは決めたくないかもしれませんし，「どうソートをしているか」はその処理の実現者以外には隠ぺいしたいかもしれないからです．このためVDMでは，操作の事前条件・事後条件だけ定めることもあります．

ただし，実際に動かしてみる方が開発者にとってイメージが持ちやすく，また「その動作によって本当に事後条件を満たす結果に必ずつながるのか」というのは，検証の対象とすべき重要な性質です．このためVDMでは操作の動作本体も記述し，仕様を実行可能とできるようになっています．

VDMにおける「実行」は，あくまで実装の詳細にこだわらず，開発の初期に仕様のプロトタイピングやテスティングを行うための「仕様の実行」です．このため一般的なプログラミング言語のように「リストがどのようにメモリ上で実現されているか」，といったことは考えませんし，抽象的な実行文を書くこともできるようになっています．例えば「リストが小さい順に並んでいたらtrue，そうでなければfalse」という計算は以下のように１つの forall 文で記述できます．
    forall i, j in set inds list1 & i < j => list1(i) <= list1(j)
（list1 のインデックスの集合からどの２つを抜き出して i ， j としても（forall ... & ... ）， i が j より小さいならば i 番目の要素は j 番目の要素以下である）

その他VDM Toolboxには，C++やJavaのコードをVDM++仕様から生成する機能等もあります．

形式手法としてのVDM

大ざっぱにまとめると，形式手法・ツールとしてのVDMおよびVDM Toolboxの特徴は下記のようになります．

バリエーション

ここで「形式仕様記述」という手法の分類は，システム状態のデータ構造やそれを操作するメソッドの機能等に関する仕様を形式化，検証する方法に対する名称です．同じ形式仕様記述であっても，VDMのようにプログラミング言語に近い記述ではなく，数式のような形でもっと抽象的な記述を行うものや，抽象度の高い記述から実装コードに至るまでの段階的な詳細化を支援するものもあります．また，「性質を検証する方法」としてツールによる（半）自動証明を用いるものもあります．

このページの先頭へ戻る