| dbpprop:abstract
|
- In theoretical computer science, correctness of an algorithm is asserted when it is said that the algorithm is correct with respect to a specification. Functional correctness refers to the input-output behaviour of the algorithm (i.e. , for each input it produces the correct output). See also program verification. A distinction is made between total correctness, which additionally requires that the algorithm terminates, and partial correctness, which simply requires that if an answer is returned it will be correct. Since there is no general solution to the halting problem, a total correctness assertion may lie much deeper. For example, if we are successively searching through integers 1, 2, 3, … to see if we can find an example of some phenomenon — say an odd perfect number — it is quite easy to write a partially correct program (use integer factorization to check n as perfect or not). But to say this program is totally correct would be to assert something currently not known in number theory. A proof would have to be a mathematical proof, assuming both the algorithm and specification are given formally. In particular it is not expected to be a correctness assertion for a given program implementing the algorithm on a given machine. That would involve such considerations as limitations on memory. A deep result in proof theory, the Curry-Howard correspondence, states that a proof of functional correctness in constructive logic corresponds to a certain program in the lambda calculus. Converting a proof in this way is called program extraction.
- Unter Korrektheit versteht man in der Informatik die Eigenschaft eines Computerprogramms, einer Spezifikation zu genügen. Spezialgebiete der Informatik, die sich mit dieser Eigenschaft befassen, sind die Formale Semantik und die Berechenbarkeitstheorie. Nicht abgedeckt vom Begriff Korrektheit ist, ob die Spezifikation die vom Programm zu lösende Aufgabe korrekt beschreibt (siehe dazu Validierung). Ein Programmcode wird bezüglich einer Vorbedingung P und der Nachbedingung Q partiell korrekt genannt, wenn bei einer Eingabe, die die Vorbedingung P erfüllt, jedes Ergebnis die Nachbedingung Q erfüllt. Dabei ist es noch möglich, dass das Programm nicht für jede Eingabe ein Ergebnis liefert, also nicht terminiert. Ein Code wird total korrekt genannt, wenn er partiell korrekt ist und zusätzlich für jede Eingabe, die die Vorbedingung P erfüllt, terminiert. Aus der Definition folgt sofort, dass total korrekte Programme auch immer partiell korrekt sind. Der Nachweis partieller Korrektheit (Verifikation) kann z. B. mit dem wp-Kalkül erfolgen. Um zu zeigen, dass ein Programm total korrekt ist, muss hier der Beweis der Terminierung in einem gesonderten Schritt behandelt werden. Mit dem Hoare-Kalkül kann die totale Korrektheit in vielen Fällen nachgewiesen werden. Der Nachweis der Korrektheit eines Programms kann jedoch nicht in allen Fällen geführt werden: das folgt aus dem Halteproblem bzw. aus dem Gödelschen Unvollständigkeitssatz. Auch wenn die Korrektheit für Programme, die bestimmten Einschränkungen unterliegen, bewiesen werden kann, so zählt die Korrektheit von Programmen allgemein zu den nicht-berechenbaren Problemen. Die Durchführung einer Überprüfung auf Korrektheit bezeichnet man als Beweis. Dabei ist ein Beweis der totalen Korrektheit ein Spezialfall eines mathematischen Beweises, erlaubt also im Gegensatz zum umgangssprachlichen Beweisbegriff eine absolute Aussage.
- 計算機科学における正当性（Correctness）とは、アルゴリズムがその仕様記述に照らして正しいことを意味する。「機能的」正当性とは、アルゴリズムの入出力動作に関する正当性である（すなわち、各入力に対して正しく出力を生成すること）。形式的検証を参照されたい。 完全正当性（Total Correctness）は、アルゴリズムが常に停止することも要求される。一方、部分正当性（Partial Correctness）は単に返ってくる答えが正しいことのみを要求する（常に答えが返ってくるとは限らない）。停止問題には汎用的解法はないので、完全正当性はより深い問題をはらんでいる。 例えば、整数を 1 から順に調べて奇数の完全数を探すとした場合、部分正当性を備えたプログラムを書くのは極めて簡単である（素因数分解を行って n が完全数かどうかを調べる）。しかし、そのプログラムが完全正当性を備えているとするには数論において未知の知識を必要とする。 正当性の証明は数学的証明でなければならず、アルゴリズムもその仕様記述も形式的に与えられなければならない。特にその証明は、そのアルゴリズムを特定のマシン上でプログラムとして実装したものについて正当性を意味するものではない。その場合メモリ量の限界を考慮する必要がある。 証明論におけるカリー・ハワード対応は、直観主義論理における機能的正当性の証明がラムダ計算にける特定プログラムに対応するとしている。このような証明の変換を「プログラム抽出; program extraction」と呼ぶ。
|
| rdfs:comment
|
- In theoretical computer science, correctness of an algorithm is asserted when it is said that the algorithm is correct with respect to a specification. Functional correctness refers to the input-output behaviour of the algorithm (i.e. , for each input it produces the correct output). See also program verification.
- Unter Korrektheit versteht man in der Informatik die Eigenschaft eines Computerprogramms, einer Spezifikation zu genügen. Spezialgebiete der Informatik, die sich mit dieser Eigenschaft befassen, sind die Formale Semantik und die Berechenbarkeitstheorie. Nicht abgedeckt vom Begriff Korrektheit ist, ob die Spezifikation die vom Programm zu lösende Aufgabe korrekt beschreibt (siehe dazu Validierung).
|
![[RDF Data]](/statics/sw-cube.png)
