正当性

計算機科学における正当性（Correctness）とは、アルゴリズムがその仕様に照らして正しいことを意味する。「機能的」正当性とは、アルゴリズムの入出力動作に関する正当性である（すなわち、各入力に対して正しく出力を生成すること）。形式的検証を参照されたい。 完全正当性（Total Correctness）は、アルゴリズムが常に停止することも要求される。一方、部分正当性（Partial Correctness）は単に返ってくる答えが正しいことのみを要求する（常に答えが返ってくるとは限らない）。停止問題には汎用的解法はないので、完全正当性はより深い問題をはらんでいる。 例えば、整数を 1 から順に調べて奇数の完全数を探すとした場合、部分正当性を備えたプログラムを書くのは極めて簡単である（素因数分解を行って n が完全数かどうかを調べる）。しかし、そのプログラムが完全正当性を備えているとするには数論において未知の知識を必要とする。 正当性の証明は数学的証明でなければならず、アルゴリズムもその仕様記述も形式的に与えられなければならない（形式的仕様記述）。特にその証明は、そのアルゴリズムを特定のマシン上でプログラムとして実装したものについて正当性を意味するものではない。その場合メモリ量の限界を考慮する必要がある。 証明論におけるカリー・ハワード対応は、直観主義論理における機能的正当性の証明がラムダ計算における特定プログラムに対応するとしている。このような証明の変換を「プログラム抽出; program extraction」と呼ぶ。