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.
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).
Hoare logic is a specific formal system for reasoning rigorously about the correctness of computer programs.
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.