Correctness (computer science)

Correctness (computer science)

In theoretical computer science, correctness of an algorithm is asserted when it is said that the algorithm is correct with respect to a specification. Functional correctness refers to the input-output behaviour of the algorithm (i.e., for each input it produces the correct output).

A distinction is made between total correctness, which additionally requires that the algorithm terminates, and partial correctness, which simply requires that if an answer is returned it will be correct. Since there is no general solution to the halting problem, a total correctness assertion may lie much deeper. A termination proof is a type of mathematical proof that plays a critical role in formal verification because total correctness of an algorithm depends on termination.

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 (using long division by two to check n as perfect or not). 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, 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. It can only show partial correctness and has to be augmented with a separate termination proof.

See also


Wikimedia Foundation. 2010.

Игры ⚽ Поможем сделать НИР

Look at other dictionaries:

  • computer science — computer scientist. the science that deals with the theory and methods of processing information in digital computers, the design of computer hardware and software, and the applications of computers. [1970 75] * * * Study of computers, their… …   Universalium

  • Invariant (computer science) — In computer science, a predicate that, if true, will remain true throughout a specific sequence of operations, is called (an) invariant to that sequence.UseAlthough computer programs are typically mainly specified in terms of what they change, it …   Wikipedia

  • Concurrency (computer science) — The Dining Philosophers , a classic problem involving concurrency and shared resources In computer science, concurrency is a property of systems in which several computations are executing simultaneously, and potentially interacting with each… …   Wikipedia

  • Assignment (computer science) — In computer programming, an assignment statement sets or re sets the value stored in the storage location(s) denoted by a variable name. In most imperative computer programming languages, assignment statements are one of the basic statements.… …   Wikipedia

  • On the Cruelty of Really Teaching Computer Science — “On the Cruelty of Really Teaching Computing Science” is a 1988 paper by E. W. Dijkstra[1] which argues that computer programming should be understood as a branch of mathematics, and that the formal provability of a program is a major criterion… …   Wikipedia

  • The Cruelty of Really Teaching Computer Science — “The Cruelty of Really Teaching Computing Science” is a 1988 paper by E. W. Dijkstra, which argues that computer programming should be understood as a branch of mathematics, and that the formal provability of a program is a major criterion for… …   Wikipedia

  • Correctness — may refer to: Ethics ie. moral correctness, knowledge of right and wrong Correctness (theology), a religious concept Correctness (computer science) is a concept in theoretical computer science. Political correctness, a sociolinguistic concept… …   Wikipedia

  • Garbage collection (computer science) — This article is about garbage collection in memory management. For garbage collection in an SSD, see garbage collection (SSD). For other uses, see garbage collection. In computer science, garbage collection (GC) is a form of automatic memory… …   Wikipedia

  • Referential transparency (computer science) — Referential transparency and referential opaqueness are properties of parts of computer programs. An expression is said to be referentially transparent if it can be replaced with its value without changing the program (in other words, yielding a… …   Wikipedia

  • Schedule (computer science) — In the fields of databases and transaction processing (transaction management), a schedule (also called history) of a system is an abstract model to describe execution of transactions running in the system. Often it is a list of operations… …   Wikipedia

Share the article and excerpts

Direct link
… Do a right-click on the link above
and select “Copy Link”