Loading article…
理論計算機科学 では、アルゴリズムが仕様どおりに動作する場合、そのアルゴリズムは仕様に関して正しいと言えます。最もよく研究されているのは機能的正しさであり、これはアルゴリズムの入出力動作を指します。つまり、各入力に対して、仕様を満たす出力を生成します。[ 1 ]
後者の概念では、部分的な正しさ（返された答えが正しいことを要求する）は、完全な正しさ（さらに、最終的に答えが返されること、つまりアルゴリズムが終了することを要求する）とは区別されます。同様に、プログラムの完全な正しさを証明するには、その部分的な正しさと終了性を証明すれば十分です。[ 2 ] 後者の種類の証明（終了性の証明）は、停止問題が決定不能であるため、完全に自動化することはできません。
例えば、正の整数（1、2、3、…）を順に調べて奇数の完全数を見つけるかどうかを調べるプログラムは簡単に書けますし、そのような数が存在するならば奇数の完全数を見つけるという、部分的に正しいプログラムです（囲み記事を参照）。しかし、このプログラムが完全に正しい（つまり、そのような数を見つけて終了する）と言うことは、奇数の完全数が実際に存在すると主張することになりますが、これは現在の数論では知られていません。
証明は、アルゴリズムと仕様の両方が正式に与えられていることを前提として、数学的な証明でなければならない。特に、特定のコンピュータ上でアルゴリズムを実装する特定のプログラムに対する正当性の主張は想定されていない。そのような主張には、コンピュータのメモリ容量の制限といった考慮事項が含まれるからである。
証明論における重要な結果であるカリー・ハワード対応は、構成論理における関数正当性の証明が、ラムダ計算における特定のプログラムに対応することを述べている。このように証明を変換することをプログラム抽出と呼ぶ。
ホア論理は、コンピュータプログラムの正しさについて厳密に推論するための特定の形式体系です。 [ 3 ]プログラミング言語の意味論を定義し、ホアトリプルと呼ばれる主張を通してプログラムの正しさについて議論するために公理的手法を使用します。
ソフトウェアテストとは、プログラムやシステムの属性や機能を評価し、それが要求される結果を満たしているかどうかを判断することを目的としたあらゆる活動です。ソフトウェアテストはソフトウェアの品質にとって非常に重要であり、プログラマやテスターによって広く利用されていますが、ソフトウェアの原理に対する理解が限られているため、依然として一種の技術となっています。ソフトウェアテストの難しさは、ソフトウェアの複雑さに起因します。中程度の複雑さのプログラムを完全にテストすることはできません。テストはデバッグだけではありません。テストの目的は、品質保証、検証と妥当性確認、または信頼性評価です。テストは汎用的な指標としても使用できます。正確性テストと信頼性テストは、テストの2つの主要な領域です。ソフトウェアテストは、予算、時間、品質の間のトレードオフです。[ 4 ]