Hoare logic: Difference between revisions
Content deleted Content added
well, it's a start... sort of... |
|||
| Line 1: | Line 1: | ||
'''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 program]]s. |
'''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 program]]s. |
||
Let ''C'' be a line, or sequence of lines, in a computer program, and let ''P'' and ''Q'' be [[logic]]al [[predicate]]s such that if ''P'' is true before ''C'' is executed then ''Q'' will necessarily be true after ''C'' is executed. Then the following expression |
Let ''C'' be a line, or sequence of lines, in a computer program, and let ''P'' and ''Q'' be [[logic]]al [[predicate]]s such that if ''P'' is true before ''C'' is executed then ''Q'' will necessarily be true after ''C'' is executed. Then the following expression |
||
Revision as of 15:19, 13 February 2003
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.
Further reading
- C. A. R. Hoare. "An axiomatic basis for computer programming". Communications of the ACM, 12(10):576-585, October 1969.