Karl Jones: 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..."

2016-08-31T22:19:38Z

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..."

New page

'''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 (computer science)|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 [[Flowchart|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 ==

* [https://en.wikipedia.org/wiki/Hoare_logic Hoare logic] @ Wikipedia.org

[[Category:Computer science]]
[[Category:Logic]]

Hoare logic - Revision history

Karl Jones: 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..."