このページでは，一般に言われている形式手法・ツールの利点・期待と欠点・限界に関して議論します．様々な手法・ツールがありますが，このページでは，共通した「解決しようとしている問題」「活用のために必要なこと」「対象外である問題」などを，近年の動向に触れながら整理します．
ソフトウェア開発における問題点は，個々の企業やチーム，プロジェクトにより異なりますし，形式手法・ツールが「誰にでも必ず有効な特効薬」になるわけではありません．結局「自身の問題を整理し，それに対し有効な手法・ツールの適用を検討し，試行錯誤しながら問題を解決する」ことになります．個々の形式手法・ツールの思想やサポートは様々ですが，以下では形式手法・ツールに目を向ける第一歩として，共通する利点・期待と欠点・限界について述べます．
利点・期待
個々の手法・ツールが焦点を当てている問題点，側面や開発のフェーズは異なりますが，形式手法・ツールの利点は，端的には以下の二点に集約できます．
-
要求・仕様や設計といった中間成果物を，その時点でしたい・できるレベルで明確化する．これにより，中間成果物の質を高めたり，曖昧さを取り除いて理解を深め確実に共有できるようにしたりする．つまり，コストをより早い段階に多くかけるようにし，その分，後で発覚する誤りや誤解に起因する手戻りコストや，実装やテスト段階におけるコストを減少する．
-
信頼性が求められるシステム，特に並行・分散システムなど複雑なシステムにおいて，数学的な理論に基づき，完全性や網羅性を指向したより強力な検証手段を提供する．
また，ソフトウェアシステムに関する昨今の事件や事例などから，形式手法・ツールに対する期待が高まっていることが感じられます．
-
日本国内では，ソフトウェアシステムの信頼性が強く求められている状況や，フェリカネットワークスによるVDMの適用事例などもあって，（欧米に遅ればせながら）注目されている．
-
情報セキュリティの評価基準（Common Criteria）における要件に（準）形式手法の適用が含まれるなど，高信頼システムの構築に関わる開発者にとって無視できないものとなってきている．
-
モデル検査手法は，テスティングでは除くことのできない誤りを検出する手段として特に注目されている．設計の複雑な部分に絞って，設計の検証強化として導入しやすい．
-
フェリカネットワークスの事例があること，ツールを日本のCSKシステムズが所有していることから，形式仕様記述においてはVDMが著名である．また別のライトウェイトな手法としてAlloyも注目されている．
欠点・限界
「形式手法・ツールは万能であり，それを適用すればよい」ということはありません．以下ではまず，本質的に「そもそも目指していないところ」を明確にします．
-
「ツールに任せれば完璧な検証を自動的にしてくれる」ということはない．あくまで「人が与えた明確な基準に照らし合わせる」ということがツールの役割である．ツールにわかる言葉（言語）を用いてツールに伝える（入力する）こと，その分析や検証の結果に意味づけすることは，あくまで最終的には人間が負うことになる．
-
形式手法・ツールは，原則として「決定したものを明確化，確認，分析，検証する」ための手法・ツールである．「よい決定をする」ためには別の考え方に基づくべきである．要求レベルであれば，ドメイン分析やゴール指向要求分析などの手法を用いるべきである．設計レベルであれば，オブジェクト指向・コンポーネント指向の設計論やデザインパターンなどの手法を用いるべきである．
また，形式手法・ツールは大学にしろ企業にしろ，研究機関が主となって開発を進めてきたものであるため，少なくとも今のところ「一般の開発者への必要性やノウハウ・知識の浸透」「使いやすさ」「情報の多さ」はとても十分とは言えません．この観点から「現状の」欠点について触れておきます．
-
仕様や設計のレベルで必要な情報のみを厳密に書くという抽象化の考え方や，数学的な検証の仕組みに関する理解が求められる．これらが「普通の人には難しい」かというと，そうでもないという主張も多い（プログラミングより簡単だという主張も多い）．ただ，現状では一般的な開発者はこれらのノウハウや知識に関する教育を受けておらず，「追加で」学習する必要がある．現在議論されている大学におけるソフトウェア工学教育カリキュラムのように，求められる（そして教えられる）ノウハウや知識が変わってくれば，状況が変わることが期待される．
-
全般的に情報，特に日本語の情報が少ない．また，ツールもGUIやドキュメント等使いやすさの観点では，Javaなどに関するメジャーなツールを使っている開発者には不満が多いかもしれない．「求められるから技術・ツールが発展する」というところがあり，完成度が高いツールには実際のプロジェクト適用の中で改良されてきたものが多い．これも技術的な問題というより，社会的な風潮，経済的な戦略などの問題であるため，将来変わるかもしれない．
-
適用の効果が計りづらい．これは形式手法・ツールに限らないが，ソフトウェア開発は事例ごとに背景や規模，達成目標などが異なるため，一概に「絶対こう」とは言えない．個々の事例では「これだけの人月でできた」「テスティングコストをこれだけ省けた」という報告があるが，主に論文が発表媒体となってしまっているため目立たないところがある．
ここまで非常に一般的に，抽象的に形式手法・ツールについて説明してきました．興味を持たれた方は，ぜひ参考文献や，個々の手法・ツールの解説も参照いただければと思います．
このページの先頭へ戻る