theoretical computer science Theoretical computer science is a subfield of computer science and mathematics that focuses on the Abstraction, abstract and mathematical foundations of computation. It is difficult to circumscribe the theoretical areas precisely. The Associati ...

, an

algorithm In mathematics and computer science, an algorithm () is a finite sequence of Rigour#Mathematics, mathematically rigorous instructions, typically used to solve a class of specific Computational problem, problems or to perform a computation. Algo ...

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. 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 In computability theory (computer science), computability theory, the halting problem is the problem of determining, from a description of an arbitrary computer program and an input, whether the program will finish running, or continue to run for ...

is undecidable. For example, successively searching through

integer An integer is the number zero (0), a positive natural number (1, 2, 3, ...), or the negation of a positive natural number (−1, −2, −3, ...). The negations or additive inverses of the positive natural numbers are referred to as negative in ...

s 1, 2, 3, … to see if we can find an example of some phenomenon—say an odd

perfect number In number theory, a perfect number is a positive integer that is equal to the sum of its positive proper divisors, that is, divisors excluding the number itself. For instance, 6 has proper divisors 1, 2 and 3, and 1 + 2 + 3 = 6, so 6 is a perfec ...

—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 Number theory is a branch of pure mathematics devoted primarily to the study of the integers and arithmetic functions. Number theorists study prime numbers as well as the properties of mathematical objects constructed from integers (for example ...

. 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 Computer memory stores information, such as data and programs, for immediate use in the computer. The term ''memory'' is often synonymous with the terms ''RAM,'' ''main memory,'' or ''primary storage.'' Archaic synonyms for main memory include ...

. A deep result in

proof theory Proof theory is a major branchAccording to , proof theory is one of four domains mathematical logic, together with model theory, axiomatic set theory, and recursion theory. consists of four corresponding parts, with part D being about "Proof The ...

, the Curry–Howard correspondence, states that a proof of functional correctness in constructive logic corresponds to a certain program in the

lambda calculus In mathematical logic, the lambda calculus (also written as ''λ''-calculus) is a formal system for expressing computability, computation based on function Abstraction (computer science), abstraction and function application, application using var ...

. Converting a proof in this way is called ''program extraction''. Hoare logic is a specific

formal system A formal system is an abstract structure and formalization of an axiomatic system used for deducing, using rules of inference, theorems from axioms. In 1921, David Hilbert proposed to use formal systems as the foundation of knowledge in ma ...

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 Software testing is the act of checking whether software satisfies expectations. Software testing can provide objective, independent information about the Quality (business), quality of software and the risk of its failure to a User (computin ...

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.

Notes

References

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. 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. {{Software quality Formal methods terminology Theoretical computer science Software quality

See also

Notes

References