@prefix owl: . @prefix dbpedia: . dbpedia:Correctness owl:sameAs . @prefix foaf: . @prefix ns3: . dbpedia:Correctness foaf:page ns3:Correctness . @prefix rdfs: . dbpedia:Correctness rdfs:label "Korrektheit (Informatik)"@de , "Correctness"@en , "\u6B63\u5F53\u6027 (\u8A08\u7B97\u6A5F\u79D1\u5B66)"@ja . @prefix dbpprop: . dbpedia:Correctness dbpprop:abstract "Unter Korrektheit versteht man in der Informatik die Eigenschaft eines Computerprogramms, einer Spezifikation zu gen\u00FCgen. 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\u00F6sende Aufgabe korrekt beschreibt (siehe dazu Validierung). Ein Programmcode wird bez\u00FCglich einer Vorbedingung P und der Nachbedingung Q partiell korrekt genannt, wenn bei einer Eingabe, die die Vorbedingung P erf\u00FCllt, jedes Ergebnis die Nachbedingung Q erf\u00FCllt. Dabei ist es noch m\u00F6glich, dass das Programm nicht f\u00FCr jede Eingabe ein Ergebnis liefert, also nicht terminiert. Ein Code wird total korrekt genannt, wenn er partiell korrekt ist und zus\u00E4tzlich f\u00FCr jede Eingabe, die die Vorbedingung P erf\u00FCllt, 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\u00FCl 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\u00FCl kann die totale Korrektheit in vielen F\u00E4llen nachgewiesen werden. Der Nachweis der Korrektheit eines Programms kann jedoch nicht in allen F\u00E4llen gef\u00FChrt werden: das folgt aus dem Halteproblem bzw. aus dem G\u00F6delschen Unvollst\u00E4ndigkeitssatz. Auch wenn die Korrektheit f\u00FCr Programme, die bestimmten Einschr\u00E4nkungen unterliegen, bewiesen werden kann, so z\u00E4hlt die Korrektheit von Programmen allgemein zu den nicht-berechenbaren Problemen. Die Durchf\u00FChrung einer \u00DCberpr\u00FCfung 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 , "\u8A08\u7B97\u6A5F\u79D1\u5B66\u306B\u304A\u3051\u308B\u6B63\u5F53\u6027\uFF08Correctness\uFF09\u3068\u306F\u3001\u30A2\u30EB\u30B4\u30EA\u30BA\u30E0\u304C\u305D\u306E\u4ED5\u69D8\u8A18\u8FF0\u306B\u7167\u3089\u3057\u3066\u6B63\u3057\u3044\u3053\u3068\u3092\u610F\u5473\u3059\u308B\u3002\u300C\u6A5F\u80FD\u7684\u300D\u6B63\u5F53\u6027\u3068\u306F\u3001\u30A2\u30EB\u30B4\u30EA\u30BA\u30E0\u306E\u5165\u51FA\u529B\u52D5\u4F5C\u306B\u95A2\u3059\u308B\u6B63\u5F53\u6027\u3067\u3042\u308B\uFF08\u3059\u306A\u308F\u3061\u3001\u5404\u5165\u529B\u306B\u5BFE\u3057\u3066\u6B63\u3057\u304F\u51FA\u529B\u3092\u751F\u6210\u3059\u308B\u3053\u3068\uFF09\u3002\u5F62\u5F0F\u7684\u691C\u8A3C\u3092\u53C2\u7167\u3055\u308C\u305F\u3044\u3002 \u5B8C\u5168\u6B63\u5F53\u6027\uFF08Total Correctness\uFF09\u306F\u3001\u30A2\u30EB\u30B4\u30EA\u30BA\u30E0\u304C\u5E38\u306B\u505C\u6B62\u3059\u308B\u3053\u3068\u3082\u8981\u6C42\u3055\u308C\u308B\u3002\u4E00\u65B9\u3001\u90E8\u5206\u6B63\u5F53\u6027\uFF08Partial Correctness\uFF09\u306F\u5358\u306B\u8FD4\u3063\u3066\u304F\u308B\u7B54\u3048\u304C\u6B63\u3057\u3044\u3053\u3068\u306E\u307F\u3092\u8981\u6C42\u3059\u308B\uFF08\u5E38\u306B\u7B54\u3048\u304C\u8FD4\u3063\u3066\u304F\u308B\u3068\u306F\u9650\u3089\u306A\u3044\uFF09\u3002\u505C\u6B62\u554F\u984C\u306B\u306F\u6C4E\u7528\u7684\u89E3\u6CD5\u306F\u306A\u3044\u306E\u3067\u3001\u5B8C\u5168\u6B63\u5F53\u6027\u306F\u3088\u308A\u6DF1\u3044\u554F\u984C\u3092\u306F\u3089\u3093\u3067\u3044\u308B\u3002 \u4F8B\u3048\u3070\u3001\u6574\u6570\u3092 1 \u304B\u3089\u9806\u306B\u8ABF\u3079\u3066\u5947\u6570\u306E\u5B8C\u5168\u6570\u3092\u63A2\u3059\u3068\u3057\u305F\u5834\u5408\u3001\u90E8\u5206\u6B63\u5F53\u6027\u3092\u5099\u3048\u305F\u30D7\u30ED\u30B0\u30E9\u30E0\u3092\u66F8\u304F\u306E\u306F\u6975\u3081\u3066\u7C21\u5358\u3067\u3042\u308B\uFF08\u7D20\u56E0\u6570\u5206\u89E3\u3092\u884C\u3063\u3066 n \u304C\u5B8C\u5168\u6570\u304B\u3069\u3046\u304B\u3092\u8ABF\u3079\u308B\uFF09\u3002\u3057\u304B\u3057\u3001\u305D\u306E\u30D7\u30ED\u30B0\u30E9\u30E0\u304C\u5B8C\u5168\u6B63\u5F53\u6027\u3092\u5099\u3048\u3066\u3044\u308B\u3068\u3059\u308B\u306B\u306F\u6570\u8AD6\u306B\u304A\u3044\u3066\u672A\u77E5\u306E\u77E5\u8B58\u3092\u5FC5\u8981\u3068\u3059\u308B\u3002 \u6B63\u5F53\u6027\u306E\u8A3C\u660E\u306F\u6570\u5B66\u7684\u8A3C\u660E\u3067\u306A\u3051\u308C\u3070\u306A\u3089\u305A\u3001\u30A2\u30EB\u30B4\u30EA\u30BA\u30E0\u3082\u305D\u306E\u4ED5\u69D8\u8A18\u8FF0\u3082\u5F62\u5F0F\u7684\u306B\u4E0E\u3048\u3089\u308C\u306A\u3051\u308C\u3070\u306A\u3089\u306A\u3044\u3002\u7279\u306B\u305D\u306E\u8A3C\u660E\u306F\u3001\u305D\u306E\u30A2\u30EB\u30B4\u30EA\u30BA\u30E0\u3092\u7279\u5B9A\u306E\u30DE\u30B7\u30F3\u4E0A\u3067\u30D7\u30ED\u30B0\u30E9\u30E0\u3068\u3057\u3066\u5B9F\u88C5\u3057\u305F\u3082\u306E\u306B\u3064\u3044\u3066\u6B63\u5F53\u6027\u3092\u610F\u5473\u3059\u308B\u3082\u306E\u3067\u306F\u306A\u3044\u3002\u305D\u306E\u5834\u5408\u30E1\u30E2\u30EA\u91CF\u306E\u9650\u754C\u3092\u8003\u616E\u3059\u308B\u5FC5\u8981\u304C\u3042\u308B\u3002 \u8A3C\u660E\u8AD6\u306B\u304A\u3051\u308B\u30AB\u30EA\u30FC\u30FB\u30CF\u30EF\u30FC\u30C9\u5BFE\u5FDC\u306F\u3001\u76F4\u89B3\u4E3B\u7FA9\u8AD6\u7406\u306B\u304A\u3051\u308B\u6A5F\u80FD\u7684\u6B63\u5F53\u6027\u306E\u8A3C\u660E\u304C\u30E9\u30E0\u30C0\u8A08\u7B97\u306B\u3051\u308B\u7279\u5B9A\u30D7\u30ED\u30B0\u30E9\u30E0\u306B\u5BFE\u5FDC\u3059\u308B\u3068\u3057\u3066\u3044\u308B\u3002\u3053\u306E\u3088\u3046\u306A\u8A3C\u660E\u306E\u5909\u63DB\u3092\u300C\u30D7\u30ED\u30B0\u30E9\u30E0\u62BD\u51FA; program extraction\u300D\u3068\u547C\u3076\u3002"@ja , "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, \u2026 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."@en ; 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."@en , "Unter Korrektheit versteht man in der Informatik die Eigenschaft eines Computerprogramms, einer Spezifikation zu gen\u00FCgen. 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\u00F6sende Aufgabe korrekt beschreibt (siehe dazu Validierung)."@de , ""@ja . @prefix skos: . dbpedia:Correctness skos:subject . @prefix ns7: . dbpedia:Correctness skos:subject ns7:Formal_methods . @prefix ns8: . dbpedia:Correctness dbpprop:hasPhotoCollection ns8:Correctness . dbpprop:disambiguates dbpedia:Correctness . dbpedia:Correctly dbpprop:redirect dbpedia:Correctness . dbpedia:Correctness_proof dbpprop:redirect dbpedia:Correctness . dbpedia:Aright dbpprop:redirect dbpedia:Correctness . dbpedia:Rightness dbpprop:redirect dbpedia:Correctness . dbpedia:Partial_algorithm dbpprop:redirect dbpedia:Correctness . dbpedia:Partial_correctness dbpprop:redirect dbpedia:Correctness . dbpedia:Provably_correct dbpprop:redirect dbpedia:Correctness . dbpedia:Total_correctness dbpprop:redirect dbpedia:Correctness . dbpedia:Proof_of_correctness dbpprop:redirect dbpedia:Correctness . dbpedia:Rightly dbpprop:redirect dbpedia:Correctness . dbpedia:Correct dbpprop:redirect dbpedia:Correctness . dbpedia:Program_correctness dbpprop:redirect dbpedia:Correctness .