Hoare logic

E100208
axiomatic semantics formal system program logic

Hoare logic is a formal system in computer science used to reason rigorously about the correctness of computer programs using logical assertions about program states.

Try in SPARQL Jump to: Surface forms Statements Referenced by

All labels observed (4)

Label Occurrences
Hoare logic canonical 6
Floyd–Hoare logic 1
Hoare triple 1

Statements (49)

Predicate Object
instanceOf axiomatic semantics ⓘ
formal system ⓘ
program logic ⓘ
appliesTo imperative programs ⓘ
assumes formal semantics of the programming language ⓘ
basedOn first-order logic ⓘ
coreConcept Hoare triple ⓘ
describedIn An Axiomatic Basis for Computer Programming ⓘ
field computer science ⓘ
formal methods ⓘ
program verification ⓘ
formalizes reasoning with assertions about program states ⓘ
hasExtension dynamic logic-based systems ⓘ
probabilistic Hoare logic ⓘ
separation logic ⓘ
hasProperty relative completeness ⓘ
soundness ⓘ
hasRule assignment axiom ⓘ
conditional rule ⓘ
consequence rule ⓘ
sequence rule ⓘ
while rule ⓘ
influenced design of specification languages ⓘ
development of separation logic ⓘ
dynamic logic ⓘ
program verification research ⓘ
introducedBy Tony Hoare ⓘ
surface form: C. A. R. Hoare
introducedIn 1969 ⓘ
namedAfter Tony Hoare ⓘ
surface form: C. A. R. Hoare
relatedTo Dijkstra weakest precondition calculus ⓘ
Hoare logic self-linksurface differs ⓘ
surface form: Floyd–Hoare logic

denotational semantics ⓘ
operational semantics ⓘ
representsHoareTripleAs {P} C {Q} ⓘ
supports compositional verification ⓘ
modular reasoning about programs ⓘ
taughtIn formal methods courses ⓘ
program verification courses ⓘ
typicalPostconditionForm logical formula over program variables ⓘ
typicalPreconditionForm logical formula over program variables ⓘ
usedFor proving partial correctness of programs ⓘ
proving total correctness of programs ⓘ
reasoning about program correctness ⓘ
usesConcept assertion ⓘ
invariant ⓘ
loop invariant ⓘ
postcondition ⓘ
precondition ⓘ
program state ⓘ

Referenced by (9)

Full triples — surface form annotated when it differs from this entity's canonical label.

Tony Hoare → notableWork → Hoare logic ⓘ
Tony Hoare → notableIdea → Hoare logic ⓘ
this entity surface form: Hoare triple
Dijkstra → notableConcept → Hoare logic ⓘ
this entity surface form: weakest precondition
Hoare logic → relatedTo → Hoare logic self-linksurface differs ⓘ
this entity surface form: Floyd–Hoare logic
Temporal Logic of Actions → comparedWith → Hoare logic ⓘ
Types and Programming Languages (research contributions) → influencedBy → Hoare logic ⓘ
The Logic of Computer Programming → relatedConcept → Hoare logic ⓘ
Design by Contract → relatedTo → Hoare logic ⓘ
A Discipline of Programming → relatedTo → Hoare logic ⓘ