Z言語 を使った形式仕様記述 の例形式手法 （けいしきしゅほう、英 : formal methods ）は、ソフトウェア工学 における数学 を基盤としたソフトウェア およびハードウェア システムの仕様記述 、開発、検証 の技術である[ 1] 工学 分野と同様、適切な数学的解析を行うことで設計の信頼性と頑健性が向上するという予想によって動機付けられている[ 2]
形式手法は理論計算機科学 の様々な成果を基盤として応用したものであり、数理論理学 、形式言語 、オートマタ理論 、プログラム意味論 、型システム 、代数的データ型 などを活用して、ソフトウェアおよびハードウェアの仕様記述とその検証を行う[ 3]
形式手法はいくつかの水準で使用可能である:
水準0
形式仕様記述 を行い、プログラム自体を非形式主義的に行う。「軽い形式手法」と呼ぶ。費用対効果が早く得ることができる選択である。水準1
形式手法を使って開発 と検証 を行い、より形式主義的にプログラムを生成する。例えば、仕様記述 からのプログラム 作成において詳細化 と属性の証明を行う。高信頼システムに適した選択である。
水準2
自動定理証明 によって完全に機械的な証明を行う。道具を整備するのに費用がかかるか、厳密である必要がありシステムを記述するのに手間がかかる。間違いが混入することで生じる損失に見合わなければ実施しない（例えば、マイクロプロセッサ設計の重要な部分など）。詳しくは後述 する。
プログラム意味論 の分類に対応して、形式手法は以下のように大別する:
表示的意味論 表示的意味論では、システムの意味は領域理論 で表現する。この場合、領域理論の性質によってシステムの意味を与える。しかし、あらゆるシステムが関数に直感的に表現できるわけではないとも言われている。
操作的意味論 操作的意味論では、より単純な計算モデルの一連の動作によってシステムの意味を表現する。この場合、モデルの単純性が表現を明確にする。しかし、これは意味論的な判断の先延ばしとも言われている（つまり、使用された単純な計算モデルの意味論の定義はどうなるのか？）。
公理的意味論 公理的意味論では、システムがある処理を行う前と後の（真なる）状態によってシステムの意味を表現する。この場合、古典的論理学 と関係が深い。しかし、単に実行前と実行後の状態を示しただけで実際にシステムが何をするかを表現したことになるのかとの疑念も言われている。
実際の開発に携わる人々の中には、形式手法コミュニティが仕様記述と設計の完全な形式化を強調しすぎていると感じている[ 4] [ 5] 複雑性 だけでなく使用する言語の表現能力が完全かどうかが形式化を困難にしていると主張する。代替案として様々な軽量（ライトウェイト）な形式手法が提案されてきた。それらは部分的な仕様記述と応用に注力したものである。このようなライトウェイトな形式手法の例として、型システム 、uppaal Alloy オブジェクトモデリング 記法[ 6] Z言語 によるユースケース 駆動型開発[ 7] VDM ツールセット[ 8]
形式手法は開発工程 の様々な部分に適用可能である。
形式手法は開発対象システムの任意のレベルの仕様を記述するのに利用可能である。そのような形式的記述はその後の開発活動のガイドとなるだけでなく、開発されたシステムの機能が要求通りであるか正確性と完全性の観点での検証にも利用可能である。
従来から、形式仕様記述システムの必要性は注目されている。ALGOL 58 の報告書[ 9] ジョン・バッカス はプログラミング言語 の文法の形式的記法（後にバッカス・ナウア記法 、BNF記法と呼ばれるようになった[ 10]
形式仕様記述ができると、それに従って設計 を行い、実際の開発 を行う（すなわち、ソフトウェアやハードウェアに実体化させる）。例えば:
操作的意味論 に基づく形式仕様記述の場合、実際のシステムの動作と仕様上の動作（それ自体が実行可能/シミュレート可能）を比較する。さらにツールによってはそのような仕様記述から自動的にコードを生成するものもある。公理的意味論 に基づく形式仕様記述の場合、仕様に記された事前状態と事後状態が実行コード内にアサーション として組み込まれる。
形式仕様記述ができると、それを証明 の根拠として使用することもある。
場合によっては、システムの正当性の証明を行う動機は、システムの品質保証のためではなく、システムの動作をさらに理解したいためということがある。結果として正当性の証明を数学的証明 の形式で行うこともある。自然言語 を使い、あまり形式的でない形で証明が記述される。よい証明とは、他の人間が読んで理解できるものと言える。
このような手法への批判として、自然言語の曖昧 さがエラーを見逃す原因となるとの指摘がある。微妙なエラーはそのような証明で見過ごされた低レベルな詳細部分に潜んでいることが多い。さらに、よい証明を作成するには高度な数学的専門知識が必要である。
一方、システムの正当性の証明を自動的に生成することに関心が集まりつつある。自動化技術は2つに分類される:
自動定理証明 では、何もないところから形式的証明を生成する。入力となるのはシステムの説明、論理的公理群、推論規則群である。モデル検査 では、実行時に取りうる全状態を検索し、一定の特性を照合する。一部の自動定理証明は人間の補助なしには機能せず、追跡すべき特性を人間が指定してやる必要がある。モデル検査ではうまく抽象化されたモデルを与えないと、膨大な数の状態によって身動きが取れなくなる。
これらシステムの提唱者は、詳細に渡ってアルゴリズム 的に照合が行われるため、その結果は人間による証明よりも数学的にずっと正確であると主張する。これらシステムを使うための訓練は手で証明を書くための訓練よりも簡単であり、多くの人材を生み出せるとしている。
批判的な人々は、それらシステムの「神託 」的性格を問題にする。それらは真実であると宣言しているが、その詳細は説明されない。また「検査機構の検査」と呼ばれる問題もある。検証に関わるプログラム自体が検証されていない場合、その結果を疑う余地があるだろう。
部分的な批評だけでなく、形式手法全体への批判もある。現状、人間の手による証明も自動的な証明も多大な時間（とお金）を要する。従って、形式手法はそのコストが十分利益に見合うか、エラーの混入が多大な損害に結びつく場合にのみ使われることになる。例えば、航空宇宙工学 ではエラーの混入は死を意味するため、他の領域よりも形式手法が一般化している。
形式手法の推進者の中には、それがソフトウェア危機 の特効薬となると主張する者もあった。もちろん多くの人々はソフトウェア危機に特効薬は存在しないと考えている[ 11]
以下に主な形式手法と形式手法の記述法を列挙する。
仕様記述言語
モデルチェッカ
^ R. W. Butler (2001年8月6日). “What is Formal Methods? ”. 2006年11月16日閲覧。 ^ C. Michael Holloway. Why Engineers Should Consider Formal Methods オリジナル の2006年11月16日時点におけるアーカイブ。. https://web.archive.org/web/20061116210448/http://klabs.org/richcontent/verification/holloway/nasa-97-16dasc-cmh.pdf 2006年11月16日閲覧。 . ^ Monin & Hinchey 2003 , pp. 3–4^ Daniel Jackson and Jeannette Wing, "Lightweight Formal Methods" , IEEE Computer , 1996年4月
^ Vinu George and Rayford Vaughn, "Application of Lightweight Formal Methods in Requirement Engineering" , Crosstalk: The Journal of Defense Software Engineering , 2003年1月
^ Daniel Jackson, "Alloy: A Lightweight Object Modelling Notation" , ACM Transactions on Software Engineering and Methodology (TOSEM) , Volume 11, Issue 2 (2002年4月), pp. 256-290
^ Richard Denney, Succeeding with Use Cases: Working Smart to Deliver Quality , Addison-Wesley Professional Publishing, 2005, ISBN 0-321-31643-6 .
^ Sten Agerholm and Peter G. Larsen, "A Lightweight Approach to Formal Methods" , In Proceedings of the International Workshop on Current Trends in Applied Formal Methods , Boppard, Germany, Springer-Verlag, 1998年10月
^ Backus, J.W. (1959). "The Syntax and Semantics of the Proposed International Algebraic Language of Zürich ACM-GAMM Conference". Proceedings of the International Conference on Information Processing . UNESCO. ^ Knuth, Donald E. (1964), Backus Normal Form vs Backus Naur Form. Communications of the ACM , 7(12):735–736.^ フレデリック・ブルックス 、『銀の弾などない 』 (No Silver Bullet ) 、1986年
Monin, Jean François; Hinchey, Michael G. (2003), Understanding formal methods , Springer , ISBN 1-85233-247-6 Jonathan P. Bowen and Michael G. Hinchey, Formal Methods . In Allen B. Tucker, Jr. (ed.), Computer Science Handbook , 2nd edition, Section XI, Software Engineering ,Chapter 106, pages 106-1 – 106-25, Chapman & Hall / CRC Press, Association for Computing Machinery , 2004.
Michael G. Hinchey, Jonathan P. Bowen, and Emil Vassev, Formal Methods . In Philip A. Laplante (ed.), Encyclopedia of Software Engineering , Taylor & Francis , 2010, pages 308–320.
この記事は2008年11月1日以前にFree On-line Dictionary of Computing から取得した項目の資料を元に、GFDL バージョン1.3以降の「RELICENSING」(再ライセンス) 条件に基づいて組み込まれている。
