いまさら聞けない 形式手法入門：品質向上技術解説（3/3 ページ）

[阿部 功二 CSKシステムズ，MONOist]

仕様記述言語

　これまで形式手法の全体像を紹介してきましたが、ここで仕様記述言語について少し具体的に見てみましょう。

プログラミング言語との違い

　形式仕様記述は、記述自体があいまいさを排除する仕組みになっています。形式仕様記述で記述された仕様は演算式などが使用され、一見プログラムのように見えます。これは、仕様を計算機で扱うのに都合がよいように数式をASCIIで表現した結果です。実際に、形式仕様記述ではツールによる検証を実現しています。

　形式仕様記述がプログラム言語に似た表記法であることから、「プログラムを書くこと」と何が違うのか疑問に思う人は多いようです。

　まず、プログラミングは「計算機の振る舞いを記述すること」が目的で、実現手段を実装することです。

　一方、形式仕様記述が記述するのは「仕様」です。そして、仕様の記述は「論理的な振る舞いを定義すること」が目的です。実装手段を問わず、場合によってはロジックの部分を記載しない抽象レベルの記述ができなければなりません。ただし、仕様を段階的に詳細化することにより、設計レベルまで詳細化することが可能です。さらに、プラットフォームに依存したレベルまで詳細化を行えば、実装と同等といえるでしょう。例えば、VDMTools（編注）はインタプリタとして動作させたり、C／C++やJavaのコードを生成することも可能になっています。

※編注：

形式仕様記述の一種であるVDM-SL／VDM++用の統合開発環境。

http://fmvdm.org/

　仕様がプログラムで処理しやすい表記法となることは、ほかにも利点があります、後工程のユニットテストやシステムテストの自動化に利用したり、辞書を形式的表現で記述することでドメインの再利用可能な資産を形成することもできます。

　例えば、ハードウェア部品の仕様をVDMで記述すれば、その仕様を基にソフトウェアを設計できます。VDMToolsを使って関数のソースコードをジェネレートすることで、人的ミスを低減することもできます。

事前条件、事後条件

　形式手法の「事前条件」「事後条件」は、Javaのアサーションの使い方と同じと考えて問題ありません。プログラムの「実行前の条件」と「実行後の条件」を明確にすることで、その間のプログラムが正しいことを証明できます。ただし、事前条件と事後条件があれば何でも正しいわけではありません。

プログラムXが、Aという事前条件の下、実行後にBという事後条件が成立すれば、プログラムXが正しい

という条件である必要があります。ただ、プログラムが正しいことを証明できなくても、事前・事後条件を設定することでプログラムが正しい可能性を高めることは可能です。

　ミッションクリティカルなシステムでは、正しいことを証明できるように仕様を組み立ててゆくべきですが、そのためには大変な労力を要するのも事実です。ソフトウェアの品質向上を目的に形式手法を用いるのであれば、証明ができるレベルの仕様でなくても十分に役に立つでしょう。

VDM++による記述例

　では、仕様記述言語の簡単な記述例を紹介しましょう。以下では、VDM++で平方根の定義を行っています。言語仕様を解説することが本稿の目的ではないので、ここでは仕様記述言語の雰囲気をつかんでいただければよいでしょう。

VDM++による簡単な記述例

　root関数にて、

パラメータがxで、結果として変数（平方根）の2乗がxとなるreal型の数が1つ存在すること

を定義しています。また、VDM++には、操作を記述しない「陰仕様」と操作まで記述する「陽仕様」があります。上記の記述例は陰仕様であるため「is not yet specified」として、操作を省略しています。

形式手法の事例

　国内においても注目が高まりつつある形式手法ですが、大規模な事例はまだそれほど多くありません。国内における最も大規模な事例は、フェリカネットワークスによる「モバイルFeliCa IC チップ」ファームウェア開発への適用です。このプロジェクトでは、VDM++を利用した仕様をテストケースを含めて約10万ステップ記述・検証し、品質とセキュリティを確保しています。

　形式手法は日本語の文献が少なく、最初のハードルが高いのは事実です。誰もがすぐに使いこなせるようになるとはいいませんが、プログラミング言語をマスターしている人であれば必ず使えるようになります。そして、ソフトウェア工学を基にした開発スタイルを身に付けることは、これからのエンジニアにとって大切なことだと思います。デスマーチプロジェクトを作らないために、この記事をきっかけにぜひ形式手法に挑戦してみてください。

	関連リンク：
⇒	Formal Methods Virtual Library
⇒	形式仕様記述「VDM」のコミュニティサイト（VDMToolsダウンロード可）
⇒	形式検証「LTSA」に関するページ（LTSA ダウンロード可）

	参考図書：
⇒	プログラム仕様記述論
⇒	ソフトウェア開発のモデル化技法
⇒	Validated Designs For Object-oriented Systems）
⇒	Concurrency: State Models & Java Programs