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: for each input, it produces an output satisfying the specification.[1]
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.[2] The latter kind of proof (termination proof) can never be fully automated, since the halting problem is undecidable.
| Partially correct C program to find the least odd perfect number, its total correctness is unknown as of 2023 |
// 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;
}
|
For example, successively searching through the positive integers (1, 2, 3, …) to see if we can find an odd perfect number is quite easy to write and is a partially correct program that would find an odd perfect number, if such a number exists (see box). However, to say this program is totally correct (i.e., that it will find such a number and terminate) would be to assert that an odd perfect number actually exists, which is 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.[3] 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 a 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.[4]
See also
edit- Formal verification
- Design by contract
- Program analysis
- Model checking
- Compiler correctness
- Program derivation
Notes
edit- ^ Dunlop, Douglas D.; Basili, Victor R. (June 1982). "A Comparative Analysis of Functional Correctness". Communications of the ACM. 14 (2): 229–244. doi:10.1145/356876.356881. S2CID 18627112.
- ^ Manna, Zohar; Pnueli, Amir (September 1974). "Axiomatic approach to total correctness of programs". Acta Informatica. 3 (3): 243–263. doi:10.1007/BF00288637. S2CID 2988073.
- ^ Hoare, C. A. R. (October 1969). "An axiomatic basis for computer programming". Communications of the ACM. 12 (10): 576–580. doi:10.1145/363235.363259. S2CID 207726175.
- ^ Pan, Jiantao (Spring 1999). "Software Testing" (coursework). Carnegie Mellon University. Retrieved 21 November 2017.
References
edit- "Human Language Technology. Challenges for Computer Science and Linguistics." Google Books. N.p., n.d. Web. 10 April 2017.
- "Security in Computing and Communications." Google Books. N.p., n.d. Web. 10 April 2017.
- "The Halting Problem of Alan Turing - A Most Merry and Illustrated Explanation." The Halting Problem of Alan Turing - A Most Merry and Illustrated Explanation. N.p., n.d. Web. 10 April 2017.
- Turner, Raymond, and Nicola Angius. "The Philosophy of Computer Science." Stanford Encyclopedia of Philosophy. Stanford University, 20 August 2013. Web. 10 April 2017.
- Dijkstra, E. W. "Program Correctness". U of Texas at Austin, Departments of Mathematics and Computer Sciences, Automatic Theorem Proving Project, 1970. Web.
