ソフトウェアの形式的検証
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2018/11/10 06:15 UTC 版)
「形式的検証」の記事における「ソフトウェアの形式的検証」の解説
ソフトウェアの形式的検証のための論理推論はさらに以下のように分類される。 1970年代のより古典的手法では、まずコードを普通に書き、続いてのステップで正しいことを検証する。 依存型プログラミング（英語版）では、関数の型がその関数の仕様（の一部）を含み、コードの型チェックによって仕様に対する正しさが保証される。完全な依存型プログラミング言語は第一の手法を特殊ケースとしてサポートする。 それとは相補的な若干異なる手法としてプログラム導出がある。その場合、正しさを保持したステップを踏んで関数仕様から効率的コードを生成する。例として Bird-Meertens Formalism (BMF) があり、"correctness by construction" の別の形態と見ることもできる。
※この「ソフトウェアの形式的検証」の解説は、「形式的検証」の解説の一部です。
「ソフトウェアの形式的検証」を含む「形式的検証」の記事については、「形式的検証」の概要を参照ください。
ウィキペディア小見出し辞書の「ソフトウェアの形式的検証」の項目はプログラムで機械的に意味や本文を生成しているため、不適切な項目が含まれていることもあります。ご了承くださいませ。
お問い合わせ。
- ソフトウェアの形式的検証のページへのリンク
