An Axiomatic Basis for Computer Programming
Tony Hoare’s seminal paper lays the groundwork for formal program verification by introducing Hoare logic, a method that uses preconditions, postconditions, and assertions to reason about program correctness.
More about Tony Hoare →
Summary
The paper presents a foundational framework for reasoning formally about the correctness of computer programs. Hoare introduces an axiomatic system—akin to methods used in mathematics like geometry—built around assertions and inference rules to prove the properties of programs. Central to this framework is the notation
P { Q } R, meaning if precondition
P holds before executing program
Q, then postcondition
R will hold afterward. The paper develops axioms for assignment, composition, and iteration, illustrating how these can rigorously ensure program behavior aligns with its specification.
Quotes from An Axiomatic Basis for Computer Programming
“The most important property of a program is whether it accomplishes the intentions of its user.”
Tony Hoare (verified)
Details
• Title: An Axiomatic Basis for Computer Programming
• Author: Tony Hoare
• Type: Article
• Journal: Communications of the ACM, Volume 12, Issue 10
• Publisher: Association for Computing Machinery (ACM)
• Publication time: October 1, 1969
• Publication place: New York, United States
• Link: https://dl.acm.org/doi/10.1145/363235.363259
People also read