VDM++によるオブジェクト指向システムの高品質設計と検証

VDM++によるオブジェクト指向システムの高品質設計と検証 (IT architects’ archive)

システムの機能仕様を客観的、厳密に分析するためのモデリング技法が「形式記法」である。本書では、1970年代にIBMウィーン研究所で開発された「VDM、ウィーン定義言語」をオブジェクト指向システムの分析向けに拡張をしたVDM++と、実行環境であるVDMToolsを用いたソフトウェアの機能仕様の分析とテストの実践について解説されている。
自動改札機の運賃計算プログラムはいかにデバッグされているのか？ 10の40乗という運賃パターンのテスト方法を開発者が解説（前編） － Publickey
今年2月に開催されたデブサミ（developers summit 2013）にて、「運賃計算の精算仕様書の妥当性検証」に用いられたという発表を聴き、興味を持って読んでみようと思った。

モデルの妥当性を検証するための3つのアプローチが、本書で紹介する技術に関連している。それらは、整合特性（integrity properties）、体系的テスト、そしてラピッドプロトタイピングと呼ばれるものである。整合特性は別名証明課題（proof obligations）という名前で知られている。これはシステムの性質の形式記述であり、VDMToolsから自動的に生成することができる。これに加えてVDMToolsは慣習的なテスト技法を用いた妥当性検証を支援する。この支援機能の中にはテストのカバレージの文章化をVDM++のレベルで直接提供するという機能も含まれている。
最後に妥当性はモデルを他のコード（例えばグラフィカルなインタフェース）と一緒に実行することによっても検証できる。実行中には様々な表明（不変条件、事前／事後条件）が自動的にチェックされる。もしいずれかの条件が成立しない場合、どの場所でどのような表明違反が発生したかが、情報とともに通知される。条件が厳密でテストが包括的であればあるほど、妥当性検証の結果がもたらすモデルへの信頼度は高くなる。

VDM++言語では、UMLモデリングと変換可能であるようなオブジェクト指向の記述言語である。ただ、特徴的なのが、メソッドを実行することができる変数の条件（：事前条件）や、実行後のインスタンス変数が満たしているべき条件（：事後条件）、そして、得られた全ての結果が満たしている条件や、xxxを満たす結果が少なくとも一つは存在することなどの「不変条件」といったものを、集合論の言葉を用いて厳密に規定できることが挙げられる。
「仕様自体を厳密に数学的に証明すること」というのは、VDM++の目指すところではない。「システム要件定義段階の要求仕様自体が曖昧な段階において、仕様策定者が期待する振る舞いを厳密に記述できること」が、最大の特徴である。
文章で記述された仕様書では「部分演算子の保護」「不変条件の保持」「充足可能性」といったものを十分検証することができない。そのために「仕様に書ききれていない部分」で想定外の振る舞いをしたり、実行時例外が発生することにもつながる。例外処理記述を羅列するのではなく、事前／事後／不変条件を集合を用いて記していくことで、解釈可能性が向上する。
そして、そのようなモデルに対してテストツールによるカバレッジを検証したり、APIを用いてプロトタイピングを行ったるすることによって、プロジェクトの上流段階で、仕様不備を早期・体系的に検知できる可能性が高まるということが、本書の最大のメッセージだと受け止めた。
デブサミで紹介された自動改札機の事例でも指摘されていたが、形式言語によるシステム仕様の厳密な検証には、それ相当の労力を費やすことになる。そのために、開発プロジェクトにおいてもコアで複雑で高い品質を求められる部分に特価をして、適用するというのが妥当な活用法なのだと理解をした。