|
Hoare logic is a formal system developed by the
British computer scientist C. A. R. Hoare, and published in his 1969 paper "An axiomatic
basis for computer programming". The purpose of the system is to provide a set of logical rules which one can use to reason about
computer programs.
Let C be a line, or sequence of lines, in a computer program, and let P and Q be logical predicates such that if P is
true before C is executed then Q will necessarily be true after C is executed. Then the following
expression
- {P} C {Q}
is an expression in Hoare logic, also known as a Hoare triple. Note that if C does not terminate, then there
is no "after", so Q can be any statement at all. This is called "partial correctness". If "C" terminates and at
termination "Q" is true, the expression exhibits "total correctness"
See also:
This article is a stub. You can
help Wikipedia by expanding it .
Further reading
|