| rdfs:comment
| - Un algorithme est correct s'il fait ce qu'on attend de lui. Plus précisément, rappelons qu'un algorithme est décrit par une spécification des données sur lesquelles l'algorithme va démarrer son calcul et une spécification du résultat produit par l'algorithme. Démontrer la correction de l'algorithme consiste à démontrer que l'algorithme retourne, quand il calcule en partant des données, un objet qui est un des résultats escomptés et qui satisfait la spécification du résultat comme énoncé dans la description de l'algorithme. (fr)
- Poprawność całkowita i częściowa algorytmu.
* WP – warunek początkowy – formuła logiczna definiująca dane wejściowe algorytmu.
* WK – warunek końcowy – formuła logiczna definiująca dane wyjściowe algorytmu uzyskane dla danych wejściowych spełniających WP. (pl)
- In theoretical computer science, an algorithm is correct with respect to a specification if it behaves as specified. Best explored is functional correctness, which refers to the input-output behavior of the algorithm (i.e., for each input it produces an output satisfying the specification). 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. (en)
- En teoría de la computación, la corrección de un algoritmo, también llamada correctitud (como adaptación de la palabra inglesa correctness), corresponde a una propiedad que distingue a un algoritmo de un procedimiento efectivo. Un algoritmo es correcto si: 1.
* Resuelve el problema computacional para el cual fue diseñado. 2.
* Para cada entrada, produce la salida deseada. 3.
* Termina en un tiempo de ejecución finito.
* Datos: Q360812 (es)
- Unter Korrektheit versteht man in der Informatik die Eigenschaft eines Computerprogramms, einer Spezifikation zu genügen (siehe auch Verifikation). 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). (de)
- 計算機科学における正当性（Correctness）とは、アルゴリズムがその仕様に照らして正しいことを意味する。「機能的」正当性とは、アルゴリズムの入出力動作に関する正当性である（すなわち、各入力に対して正しく出力を生成すること）。形式的検証を参照されたい。 完全正当性（Total Correctness）は、アルゴリズムが常に停止することも要求される。一方、部分正当性（Partial Correctness）は単に返ってくる答えが正しいことのみを要求する（常に答えが返ってくるとは限らない）。停止問題には汎用的解法はないので、完全正当性はより深い問題をはらんでいる。 例えば、整数を 1 から順に調べて奇数の完全数を探すとした場合、部分正当性を備えたプログラムを書くのは極めて簡単である（素因数分解を行って n が完全数かどうかを調べる）。しかし、そのプログラムが完全正当性を備えているとするには数論において未知の知識を必要とする。 正当性の証明は数学的証明でなければならず、アルゴリズムもその仕様記述も形式的に与えられなければならない（形式的仕様記述）。特にその証明は、そのアルゴリズムを特定のマシン上でプログラムとして実装したものについて正当性を意味するものではない。その場合メモリ量の限界を考慮する必要がある。 (ja)
- Na Ciência da computação teórica, a corretude de um algoritmo pode ser afirmada quando se diz que o algoritmo é correto com respeito à determinada especificação. O termo corretude funcional se refere ao comportamento de entrada-saída do algorítimo (isto é, para cada entrada ele produz a saída correta). Na teoria da prova, o Isomorfismo de Curry-Howard, afirma que uma prova da corretude funcional na Lógica intuicionista corresponde a um certo programa no Cálculo lambda. Converter uma prova dessa maneira é chamado extração de programa. (pt)
- 在理论计算机科学中，算法的正确性（英语：correctness）是指一个算法在程序规范下被认定为正确的判定。其中，功能正确（英语：functional correctness）针对输入输出的行为（例如：对每一个输入，算法都能给出预期的输出）。 人们将正确性分为两类。一类被称为部分正确性（英语：partial correctness），它要求在算法返回结果时这一结果是正确的；另一类被称为完全正确性（英语：total correctness），它在部分正确性的基础之上还要求算法必须能够结束。由于对于停机问题没有通用的解决方案，因此判定完全正确性的断言有着更多需要深层次研究的地方。是指一类数学证明，因为完全正确性需要证明一个算法会终止，所以它在程序的形式验证中起着至关重要的作用。 例如考虑这样一个问题：依次搜索整数列1, 2, 3, …来看是否存在某个特定现象——比如说存在一个奇数为完全数。对于这个问题而言，我们很容易写出一个部分正确的程序（直接对于每个数字做长除法判定其是否完全）。然而如果我们想证明这个程序是完全正确的，那就相当于我们在断言一个在数论里目前还未知的结论。 在算法和程序规范都是基于形式化来给出时，对正确性的证明应当为一个数学证明。然而我们并不期待能够给出特定机器上实现的特定程序的正确性断言，因为那样将需要考虑诸如内存限制在内的更多问题。 (zh)
|
| has abstract
| - Unter Korrektheit versteht man in der Informatik die Eigenschaft eines Computerprogramms, einer Spezifikation zu genügen (siehe auch Verifikation). 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 einer 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 für jede Eingabe 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 der Nicht-Entscheidbarkeit des Halteproblems 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. (de)
- In theoretical computer science, an algorithm is correct with respect to a specification if it behaves as specified. Best explored is functional correctness, which refers to the input-output behavior of the algorithm (i.e., for each input it produces an output satisfying the specification). Within the latter notion, partial correctness, requiring that if an answer is returned it will be correct, is distinguished from total correctness, which additionally requires that an answer is eventually returned, i.e. the algorithm terminates. Correspondingly, to prove a program's total correctness, it is sufficient to prove its partial correctness, and its termination. The latter kind of proof (termination proof) can never be fully automated, since the halting problem is undecidable. For example, 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 (see box). 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 computer 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. Hoare logic is a specific formal system for reasoning rigorously about the correctness of computer programs. It uses axiomatic techniques to define programming language semantics and argue about the correctness of programs through assertions known as Hoare triples. Software testing is any activity aimed at evaluating an attribute or capability of a program or system and determining that it meets its required results. Although crucial to software quality and widely deployed by programmers and testers, software testing still remains an art, due to limited understanding of the principles of software. The difficulty in software testing stems from the complexity of software: we can not completely test a program with moderate complexity. Testing is more than just debugging. The purpose of testing can be quality assurance, verification and validation, or reliability estimation. Testing can be used as a generic metric as well. Correctness testing and reliability testing are two major areas of testing. Software testing is a trade-off between budget, time and quality. (en)
- En teoría de la computación, la corrección de un algoritmo, también llamada correctitud (como adaptación de la palabra inglesa correctness), corresponde a una propiedad que distingue a un algoritmo de un procedimiento efectivo. Un algoritmo es correcto si: 1.
* Resuelve el problema computacional para el cual fue diseñado. 2.
* Para cada entrada, produce la salida deseada. 3.
* Termina en un tiempo de ejecución finito. Si cualquiera de estos tres puntos no se cumple, entonces estamos hablando de un algoritmo incorrecto, que para efectos prácticos, carece de utilidad, al no ser más que un procedimiento efectivo, es decir, una secuencia ordenada y determinista de pasos.
* Datos: Q360812 (es)
- Un algorithme est correct s'il fait ce qu'on attend de lui. Plus précisément, rappelons qu'un algorithme est décrit par une spécification des données sur lesquelles l'algorithme va démarrer son calcul et une spécification du résultat produit par l'algorithme. Démontrer la correction de l'algorithme consiste à démontrer que l'algorithme retourne, quand il calcule en partant des données, un objet qui est un des résultats escomptés et qui satisfait la spécification du résultat comme énoncé dans la description de l'algorithme. (fr)
- 計算機科学における正当性（Correctness）とは、アルゴリズムがその仕様に照らして正しいことを意味する。「機能的」正当性とは、アルゴリズムの入出力動作に関する正当性である（すなわち、各入力に対して正しく出力を生成すること）。形式的検証を参照されたい。 完全正当性（Total Correctness）は、アルゴリズムが常に停止することも要求される。一方、部分正当性（Partial Correctness）は単に返ってくる答えが正しいことのみを要求する（常に答えが返ってくるとは限らない）。停止問題には汎用的解法はないので、完全正当性はより深い問題をはらんでいる。 例えば、整数を 1 から順に調べて奇数の完全数を探すとした場合、部分正当性を備えたプログラムを書くのは極めて簡単である（素因数分解を行って n が完全数かどうかを調べる）。しかし、そのプログラムが完全正当性を備えているとするには数論において未知の知識を必要とする。 正当性の証明は数学的証明でなければならず、アルゴリズムもその仕様記述も形式的に与えられなければならない（形式的仕様記述）。特にその証明は、そのアルゴリズムを特定のマシン上でプログラムとして実装したものについて正当性を意味するものではない。その場合メモリ量の限界を考慮する必要がある。 証明論におけるカリー・ハワード対応は、直観主義論理における機能的正当性の証明がラムダ計算における特定プログラムに対応するとしている。このような証明の変換を「プログラム抽出; program extraction」と呼ぶ。 (ja)
- Poprawność całkowita i częściowa algorytmu.
* WP – warunek początkowy – formuła logiczna definiująca dane wejściowe algorytmu.
* WK – warunek końcowy – formuła logiczna definiująca dane wyjściowe algorytmu uzyskane dla danych wejściowych spełniających WP. (pl)
- Na Ciência da computação teórica, a corretude de um algoritmo pode ser afirmada quando se diz que o algoritmo é correto com respeito à determinada especificação. O termo corretude funcional se refere ao comportamento de entrada-saída do algorítimo (isto é, para cada entrada ele produz a saída correta). É feita uma distinção entre corretude total, que requer que o algoritmo tenha um fim, e corretude parcial, que requer simplesmente que se o algoritmo retornar uma resposta ela esteja correta. Uma vez que não há nenhuma solução geral para o Problema da parada, afirmar a corretude total de um algoritmo pode ser algo muito difícil. A [Análise de término] é um tipo de prova matemática que desempenha um papel muito importante na verificação formal por que a corretude total de um algoritmo depende de seu término. Por exemplo, buscando sucessivamente através dos números inteiros 1, 2, 3, … para ver se encontramos algum tipo de fenômeno — como encontrar um número perfeito — é muito fácil escrever um programa parcialmente correto. Mas para dizer que este programa é totalmente correto seria afirmar algo ainda desconhecido na teoria dos números. Uma prova teria de ser uma prova matemática, supondo que o algoritmo e a especificação estão dados formalmente. Em particular não se espera uma afirmação de corretude de um determinado programa implementando um algoritmo numa dada máquina. Pois envolveria algumas considerações como limitações na memória do computador. Na teoria da prova, o Isomorfismo de Curry-Howard, afirma que uma prova da corretude funcional na Lógica intuicionista corresponde a um certo programa no Cálculo lambda. Converter uma prova dessa maneira é chamado extração de programa. Lógica de Hoare é um Sistema formal específico com um conjunto de regras lógicas para um raciocínio rigoroso sobre a corretude na computação. (pt)
- 在理论计算机科学中，算法的正确性（英语：correctness）是指一个算法在程序规范下被认定为正确的判定。其中，功能正确（英语：functional correctness）针对输入输出的行为（例如：对每一个输入，算法都能给出预期的输出）。 人们将正确性分为两类。一类被称为部分正确性（英语：partial correctness），它要求在算法返回结果时这一结果是正确的；另一类被称为完全正确性（英语：total correctness），它在部分正确性的基础之上还要求算法必须能够结束。由于对于停机问题没有通用的解决方案，因此判定完全正确性的断言有着更多需要深层次研究的地方。是指一类数学证明，因为完全正确性需要证明一个算法会终止，所以它在程序的形式验证中起着至关重要的作用。 例如考虑这样一个问题：依次搜索整数列1, 2, 3, …来看是否存在某个特定现象——比如说存在一个奇数为完全数。对于这个问题而言，我们很容易写出一个部分正确的程序（直接对于每个数字做长除法判定其是否完全）。然而如果我们想证明这个程序是完全正确的，那就相当于我们在断言一个在数论里目前还未知的结论。 在算法和程序规范都是基于形式化来给出时，对正确性的证明应当为一个数学证明。然而我们并不期待能够给出特定机器上实现的特定程序的正确性断言，因为那样将需要考虑诸如内存限制在内的更多问题。 证明论中有一个结论柯里-霍华德同构。这一结论认为：任意一个在构造性逻辑下的功能正确性的证明都对应了一个λ演算程序。这种转换证明的方式被称为程序抽出（英文：program extraction）。 霍尔逻辑是一个具体的能够严密验证程序正确性的形式系统。它用一系列的公理来定义程序语言的语义，从而通过称之为霍尔三元组的断言来验证程序的正确性。 软件测试是指验证一个程序或系统的某些属性或能力来判断它是否达到预期目的的行为。尽管软件测试在软件质量方面起着至关重要的作用，并且被程序员和测试员们广泛采用，但由于人们对软件的认识十分有限，它仍旧是一个艰深的领域。软件测试的最大难点在于如何控制其复杂性：我们没有办法在一个合理的复杂度内完整地测试一个程序。测试不只是调试。测试的目的包括但不限于确保软件质量、验证其正确性和估算其稳定性。我们对测试的定义也可以更加一般化，其中正确性测试和稳定性测试是两个最大的研究领域。软件测试是预算、时间和软件质量的一个平衡。 (zh)
|
![[RDF Data]](/fct/images/sw-rdf-blue.png)
![[cxml]](/fct/images/cxml_doc.png)
![[csv]](/fct/images/csv_doc.png)
![[text]](/fct/images/ntriples_doc.png)
![[turtle]](/fct/images/n3turtle_doc.png)
![[ld+json]](/fct/images/jsonld_doc.png)
![[rdf+json]](/fct/images/json_doc.png)
![[rdf+xml]](/fct/images/xml_doc.png)
![[atom+xml]](/fct/images/atom_doc.png)
![[html]](/fct/images/html_doc.png)