正確性（コンピュータサイエンス）

理論計算機科学 では、アルゴリズムが仕様どおりに動作する場合、そのアルゴリズムは仕様に関して正しいとされます。最もよく研​​究されているのは機能的正しさで、これはアルゴリズムの入出力動作を指します。つまり、各入力に対して、仕様を満たす出力を生成します。^[1]

後者の概念では、返される答えが正しいことを要求する部分的な正しさは、最終的に答えが返されること、つまりアルゴリズムが終了することをさらに要求する完全な正しさとは区別されます。同様に、プログラムの完全な正しさを証明するには、部分的な正しさと停止性を証明すれば十分です。 ^[2]停止問題は決定不可能であるため、 後者の種類の証明（停止性の証明）は完全に自動化することはできません。

たとえば、整数1、2、3、… を順に検索して、ある現象 (たとえば奇数の完全数) の例が見つかるかどうかを調べる場合、部分的に正しいプログラムを書くのは非常に簡単です (ボックスを参照)。しかし、このプログラムが完全に正しいと言うことは、数論では現在知られていないことを主張することになります。

証明は、アルゴリズムと仕様の両方が正式に与えられていると仮定して、数学的な証明でなければなりません。特に、特定のマシンでアルゴリズムを実装する特定のプログラムの正しさの主張であることは期待されていません。それには、コンピュータのメモリの制限などの考慮事項が含まれます。

証明理論における深い結果であるカリー・ハワード対応は、構成的論理における機能的正しさの証明がラムダ計算における特定のプログラムに対応すると述べています。このように証明を変換することをプログラム抽出と呼びます。

ホーア論理は、コンピュータプログラムの正しさについて厳密に推論するための特定の形式体系です。 ^[3]ホーア論理は、公理的な手法を使用してプログラミング言語の意味を定義し、ホーアトリプルと呼ばれるアサーションを通じてプログラムの正しさについて議論します。

ソフトウェアテストとは、プログラムまたはシステムの属性または機能を評価し、必要な結果を満たしているかどうかを判断することを目的とした活動です。ソフトウェアの品質にとって非常に重要であり、プログラマーやテスターに​​よって広く採用されていますが、ソフトウェアの原理に対する理解が限られているため、ソフトウェアテストは依然として芸術の域を出ません。ソフトウェアテストの難しさは、ソフトウェアの複雑さに起因します。中程度の複雑さのプログラムを完全にテストすることはできません。テストは単なるデバッグではありません。テストの目的は、品質保証、検証と妥当性確認、または信頼性の推定です。テストは、一般的な測定基準としても使用できます。正確性テストと信頼性テストは、テストの2つの主要な領域です。ソフトウェアテストは、予算、時間、品質の間でトレードオフになります。^[4]

• 形式検証
• 契約による設計
• プログラム分析
• モデルチェック
• コンパイラの正確性
• プログラムの導出

• 「人間の言語技術。コンピュータサイエンスと言語学の課題。」Google ブックス。Np、nd Web。2017 年 4 月 10 日。
• 「コンピューティングと通信におけるセキュリティ」Google ブックス。Np、nd Web。2017 年 4 月 10 日。
• 「アラン・チューリングの停止問題 - 最も楽しくてわかりやすい説明」。アラン・チューリングの停止問題 - 最も楽しくてわかりやすい説明。Np、nd Web。2017 年 4 月 10 日。
• ターナー、レイモンド、ニコラ・アンギウス。「コンピュータサイエンスの哲学」スタンフォード哲学百科事典。スタンフォード大学、2013年8月20日。ウェブ。2017年4月10日。
• Dijkstra, EW「プログラムの正確性」。テキサス大学オースティン校、数学およびコンピュータ科学部、自動定理証明プロジェクト、1970 年。Web。