形式手法

読み方 : けいしきしゅほう

形式手法とは

ある規則にのっとってシステムの仕様を厳密に記述する手法。ここでの“厳密”とは、解釈が一通りしかできないことと、論理的な矛盾がないことを意味する。そのための専用言語が形式仕様記述言語であり、記述した仕様を形式仕様と呼ぶ。

仕様を日本語で記述すると、どんなに精密に書いても、複数の解釈が生まれやすい。また、一つの変数を複数の型で使っているといった矛盾や、条件分岐での抜けも起こりがち。形式仕様記述言語を使えば、それらを排除できる。結果として仕様を記述する段階で、かなりのバグをつみ取ることができる。システム開発における概要設計と詳細設計のように、機能(外部仕様)とそれを実現するための仕様(内部仕様)の両方を形式仕様記述言語で記述すれば、その間で矛盾が存在しないかどうかを検証することもできる。

形式仕様記述言語では、利用するすべてのデータの項目名と型を宣言する。その上で、状態遷移と、それぞれの状態が変わる前に成り立つべき前提条件、状態遷移の結果として成り立つべき事後条件を記述する。個々の状態遷移は一つの処理を示しており、前提条件は入力データとして取り得る値、事後条件は、出力データとして取り得る値に相当する。

出典:ITpro「今日のキーワード」(C)日経BP社

[2010年 1月 1日 公開]

大塚商会の法人向け通販サイト(たのめーる)のご紹介