Editing Correctness (computer science) (section)

{{Short description|Quality of an algorithm being correct with respect to a specification}}
{{Use dmy dates|date=April 2017}}
In [[theoretical computer science]], an [[algorithm]] is '''correct''' with respect to a [[program specification|specification]] if it behaves as specified. Best explored is ''functional'' correctness, which refers to the input–output behavior of the algorithm: for each input it produces an output satisfying the specification.<ref name="functional">{{Cite journal | last1 = Dunlop | first1 = Douglas D. | last2 = Basili | first2 = Victor R. | authorlink2 = Victor Basili | title = A Comparative Analysis of Functional Correctness | doi = 10.1145/356876.356881 | journal = [[Communications of the ACM]]| volume = 14 | issue = 2 | pages = 229&ndash;244 | date=June 1982 | s2cid = 18627112 | url = https://dl.acm.org/ft_gateway.cfm?id=356881}}</ref>

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 [[mathematical proof|prove]] a program's total correctness, it is sufficient to prove its partial correctness, and its termination.<ref name="totalcorrectness">{{Cite journal | last1 = Manna | first1 = Zohar | last2 = Pnueli | first2 = Amir | title = Axiomatic approach to total correctness of programs | doi = 10.1007/BF00288637 | journal = [[Acta Informatica]]| volume = 3 | issue = 3 | pages = 243&ndash;263 | date=September 1974 | s2cid = 2988073 }}</ref>  The latter kind of proof ([[termination proof]]) can never be fully automated, since the [[halting problem]] is [[undecidable problem|undecidable]].

{| class="wikitable collapsible" style="float:right"
|-
| Partially correct [[C (programming language)|C]] program to find<BR>the least odd perfect number,<BR>its total correctness is unknown as of 2023
|-
| <syntaxhighlight lang=C>
// return the sum of proper divisors of n
static int divisorSum(int n) {
   int i, sum = 0;
   for (i=1; i<n; ++i)
      if (n % i == 0)
         sum += i;
   return sum;
}
// return the least odd perfect number
int leastPerfectNumber(void) {
   int n;
   for (n=1; ; n+=2)
      if (n == divisorSum(n))
         return n;
}
</syntaxhighlight>
|}
For example, successively searching through [[integer]]s 1, 2, 3, … to see if we can find an example of some phenomenon&mdash;say an odd [[perfect number]]&mdash;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 [[Perfect number#Odd perfect numbers|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.<ref name="hoare">{{Cite journal | last1 = Hoare | first1 = C. A. R. | authorlink1 = C.A.R. Hoare | title = An axiomatic basis for computer programming | doi = 10.1145/363235.363259 | journal = [[Communications of the ACM]] | volume = 12 | issue = 10 | pages = 576&ndash;580 | date = October 1969  <!-- | url=http://sunnyday.mit.edu/16.355/Hoare-CACM-69.pdf --> | url = http://www.spatial.maine.edu/~worboys/processes/hoare%20axiomatic.pdf | url-status = dead | archiveurl = https://web.archive.org/web/20160304013345/http://www.spatial.maine.edu/~worboys/processes/hoare%20axiomatic.pdf | archivedate = 4 March 2016 | df = dmy-all | citeseerx = 10.1.1.116.2392 | s2cid = 207726175 }}</ref> 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.<ref>{{cite web 
 |url=http://www.ece.cmu.edu/~koopman/des_s99/sw_testing/ |title=Software Testing |last=Pan |first=Jiantao |publisher=Carnegie Mellon University |access-date=21 November 2017 |date=Spring 1999 |type=coursework}}</ref>