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
Proof most often refers to:
* Proof (truth), argument or sufficient evidence for the truth of a proposition
* Alcohol proof, a measure of an alcoholic drink's strength
Proof may also refer to:
Mathematics and formal logic
* Formal proof, a con ...
a program's total correctness, it is sufficient to prove its partial correctness, and its termination.
The latter kind of proof (
termination proof
Termination may refer to:
Science
* Termination (geomorphology), the period of time of relatively rapid change from cold, glacial conditions to warm interglacial condition
* Termination factor, in genetics, part of the process of transcribing R ...
) 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
Proof theory is a major branchAccording to Wang (1981), pp. 3–4, proof theory is one of four domains mathematical logic, together with model theory, axiomatic set theory, and recursion theory. Jon Barwise, Barwise (1978) consists of four correspo ...
, the
Curry–Howard correspondence
In programming language theory and proof theory, the Curry–Howard correspondence (also known as the Curry–Howard isomorphism or equivalence, or the proofs-as-programs and propositions- or formulae-as-types interpretation) is the direct relati ...
, states that a proof of functional correctness in
constructive logic corresponds to a certain program in the
lambda calculus
Lambda calculus (also written as ''λ''-calculus) is a formal system in mathematical logic for expressing computation based on function abstraction and application using variable binding and substitution. It is a universal model of computation ...
. Converting a proof in this way is called ''program extraction''.
Hoare logic
Hoare logic (also known as Floyd–Hoare logic or Hoare rules) is a formal system with a set of logical rules for reasoning rigorously about the correctness of computer programs. It was proposed in 1969 by the British computer scientist and log ...
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.
See also
*
Formal verification
*
Design by contract
*
Program analysis
*
Model checking
In computer science, model checking or property checking is a method for checking whether a finite-state model of a system meets a given specification (also known as correctness). This is typically associated with hardware or software systems ...
*
Compiler correctness
*
Program derivation In computer science, program derivation is the derivation of a program from its specification, by mathematical means.
To ''derive'' a program means to write a formal specification, which is usually non-executable, and then apply mathematically corr ...
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