|
形式手法（けいしきしゅほう、）は、ソフトウェア工学における数学を基盤としたソフトウェアおよびハードウェアシステムの仕様記述、開発、検証の技術である。ソフトウェアおよびハードウェア設計への形式手法の適用は、他の工学分野と同様、適切な数学的解析を行うことで設計の信頼性と頑健性が向上するという予想によって動機付けられている。 形式手法は理論計算機科学の様々な成果を基盤として応用したものであり、数理論理学、形式言語、オートマタ理論、プログラム意味論、型システム、代数的データ型などを活用して、ソフトウェアおよびハードウェアの仕様記述とその検証を行う。 == 分類 == 形式手法はいくつかの水準で使用可能である: ; 水準0 : 形式仕様記述を行い、プログラム自体を非形式主義的に行う。「軽い形式手法」と呼ぶ。費用対効果が早く得ることができる選択である。 ; 水準1 : 形式手法を使って開発と検証を行い、より形式主義的にプログラムを生成する。例えば、仕様記述からのプログラム作成において詳細化と属性の証明を行う。高信頼システムに適した選択である。 ; 水準2 : 自動定理証明によって完全に機械的な証明を行う。道具を整備するのに費用がかかるか、厳密である必要がありシステムを記述するのに手間がかかる。間違いが混入することで生じる損失に見合わなければ実施しない（例えば、マイクロプロセッサ設計の重要な部分など）。 詳しくは後述する。 プログラム意味論の分類に対応して、形式手法は以下のように大別する: ; 表示的意味論 : 表示的意味論では、システムの意味は領域理論で表現する。この場合、領域理論の性質によってシステムの意味を与える。しかし、あらゆるシステムが関数に直感的に表現できるわけではないとも言われている。 ; 操作的意味論 : 操作的意味論では、より単純な計算モデルの一連の動作によってシステムの意味を表現する。この場合、モデルの単純性が表現を明確にする。しかし、これは意味論的な判断の先延ばしとも言われている（つまり、使用された単純な計算モデルの意味論の定義はどうなるのか？）。 ; 公理的意味論 : 公理的意味論では、システムがある処理を行う前と後の（真なる）状態によってシステムの意味を表現する。この場合、古典的論理学と関係が深い。しかし、単に実行前と実行後の状態を示しただけで実際にシステムが何をするかを表現したことになるのかとの疑念も言われている。 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「形式手法」の詳細全文を読む スポンサード リンク
|