形式手法

形式手法（けいしきしゅほう、）は、ソフトウェア工学における数学を基盤としたソフトウェアおよびハードウェアシステムの仕様記述、開発、検証の技術である。ソフトウェアおよびハードウェア設計への形式手法の適用は、他の工学分野と同様、適切な数学的解析を行うことで設計の信頼性と頑健性が向上するという予想によって動機付けられている。
形式手法は理論計算機科学の様々な成果を基盤として応用したものであり、数理論理学、形式言語、オートマタ理論、プログラム意味論、型システム、代数的データ型などを活用して、ソフトウェアおよびハードウェアの仕様記述とその検証を行う。
分類.
形式手法はいくつかの水準で使用可能である:
詳しくは後述する。
プログラム意味論の分類に対応して、形式手法は以下のように大別する:
軽量(light weight)形式手法.
実際の開発に携わる人々の中には、形式手法コミュニティが仕様記述と設計の完全な形式化を強調しすぎていると感じている。彼らは対象となるシステム自体の複雑性だけでなく使用する言語の表現能力が完全かどうかが形式化を困難にしていると主張する。代替案として様々な軽量（ライトウェイト）な形式手法が提案されてきた。それらは部分的な仕様記述と応用に注力したものである。このようなライトウェイトな形式手法の例として、型システム、uppaal Alloy オブジェクトモデリング記法、Z言語によるユースケース駆動型開発、CSK VDM ツールセットがある。
利用.
形式手法は開発工程の様々な部分に適用可能である。
仕様記述.
形式手法は開発対象システムの任意のレベルの仕様を記述するのに利用可能である。そのような形式的記述はその後の開発活動のガイドとなるだけでなく、開発されたシステムの機能が要求通りであるか正確性と完全性の観点での検証にも利用可能である。
従来から、形式仕様記述システムの必要性は注目されている。ALGOL 58の報告書の中でジョン・バッカスはプログラミング言語の文法の形式的記法（後にバッカス・ナウア記法、BNF記法と呼ばれるようになった）を提案した。バッカスはプログラミング言語の意味論の記法の必要性にも言及した。報告書にはBNF記法と同様の意味論に関する記法を将来提案すると書かれているが、それが現われることはなかった。
開発.
形式仕様記述ができると、それに従って設計を行い、実際の開発を行う（すなわち、ソフトウェアやハードウェアに実体化させる）。例えば:
検証.
形式仕様記述ができると、それを証明の根拠として使用することもある。
人間による証明.
場合によっては、システムの正当性の証明を行う動機は、システムの品質保証のためではなく、システムの動作をさらに理解したいためということがある。結果として正当性の証明を数学的証明の形式で行うこともある。自然言語を使い、あまり形式的でない形で証明が記述される。よい証明とは、他の人間が読んで理解できるものと言える。
このような手法への批判として、自然言語の曖昧さがエラーを見逃す原因となるとの指摘がある。微妙なエラーはそのような証明で見過ごされた低レベルな詳細部分に潜んでいることが多い。さらに、よい証明を作成するには高度な数学的専門知識が必要である。
自動証明.
一方、システムの正当性の証明を自動的に生成することに関心が集まりつつある。自動化技術は2つに分類される:
一部の自動定理証明は人間の補助なしには機能せず、追跡すべき特性を人間が指定してやる必要がある。モデル検査ではうまく抽象化されたモデルを与えないと、膨大な数の状態によって身動きが取れなくなる。
これらシステムの提唱者は、詳細に渡ってアルゴリズム的に照合が行われるため、その結果は人間による証明よりも数学的にずっと正確であると主張する。これらシステムを使うための訓練は手で証明を書くための訓練よりも簡単であり、多くの人材を生み出せるとしている。
批判的な人々は、それらシステムの「神託」的性格を問題にする。それらは真実であると宣言しているが、その詳細は説明されない。また「検査機構の検査」と呼ばれる問題もある。検証に関わるプログラム自体が検証されていない場合、その結果を疑う余地があるだろう。
批評.
部分的な批評だけでなく、形式手法全体への批判もある。現状、人間の手による証明も自動的な証明も多大な時間（とお金）を要する。従って、形式手法はそのコストが十分利益に見合うか、エラーの混入が多大な損害に結びつく場合にのみ使われることになる。例えば、航空宇宙工学ではエラーの混入は死を意味するため、他の領域よりも形式手法が一般化している。
形式手法の推進者の中には、それがソフトウェア危機の特効薬となると主張する者もあった。もちろん多くの人々はソフトウェア危機に特効薬は存在しないと考えているし、形式手法の利点を強調しすぎる姿勢を問題にする人々もいる。
主な形式手法とその記述法.
以下に主な形式手法と形式手法の記述法を列挙する。
仕様記述言語
モデルチェッカ