Hoare logic
From Wiki @ Karl Jones dot com
Revision as of 15:19, 31 August 2016 by Karl Jones (Talk | contribs) (Created page with "'''Hoare logic''' (also known as '''Floyd–Hoare logic''' or '''Hoare rules''') is a formal system with a set of logical rules for reasoning rigorously about the Correc...")
Hoare logic (also known as Floyd–Hoare logic or Hoare rules) is a formal system with a set of logical rules for reasoning rigorously about the correctness of computer programs.
It was proposed in 1969 by the British computer scientist and logician Tony Hoare, and subsequently refined by Hoare and other researchers.
The original ideas were seeded by the work of Robert W. Floyd, who had published a similar system for flowcharts.
See also
- Assertion (computing)
- Communicating sequential processes
- Correctness (computer science)
- Design by contract
- Denotational semantics
- Dynamic logic
- Edsger W. Dijkstra
- Loop invariant
- Predicate transformer semantics
- Program verification
- Refinement calculus
- Separation logic
- Sequent calculus
- Static code analysis
External links
- Hoare logic @ Wikipedia.org
