Encyclopedia > Hoare logic

  Article Content

Hoare logic

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.

See also:

Further reading



All Wikipedia text is available under the terms of the GNU Free Documentation License

 
  Search Encyclopedia

Search over one million articles, find something about almost anything!
 
 
  
  Featured Article
Shoreham, New York

... 2.88% of the population are Hispanic or Latino of any race. There are 145 households out of which 38.6% have children under the age of 18 living with them, 74.5% ...

 
 
 
This page was created in 22.6 ms