An Axiomatic Basis for Computer Programming
đź“ś Abstract
In this paper an attempt is made to explore the logical foundations of computer programming by use of techniques which were first applied in the study of geometry and have later been extended to other branches of mathematics. This involves the elucidation of sets of axioms and rules of inference which can be used in proofs of the properties of computer programs. Examples are given of such axioms and rules, and a formal proof of a simple theorem is displayed. Finally, it is argued that important advantages, both theoretical and practical, may follow from a pursuance of these topics.
✨ Summary
Overview
C. A. R. Hoare proposes an axiomatic foundation for reasoning about imperative programs. The paper introduces assertions relating a precondition, a program, and a postcondition, written as P{Q}R, and presents an assignment axiom together with rules for logical consequence, sequential composition, and iteration. These rules allow properties of program executions to be derived deductively rather than established only through testing. The paper also gives a worked proof for a successive-subtraction division routine, establishing the quotient–remainder relationship and the remainder bound, assuming successful termination and suitable arithmetic properties. The paper’s publication details are corroborated by the ACM record. (doi.org)
A second contribution is the treatment of computer arithmetic as part of the semantic foundation of programming. Hoare distinguishes mathematical integer arithmetic from finite machine arithmetic and discusses alternative overflow behaviors, including strict failure, saturation at a maximum value, and modulo arithmetic. This anticipates the need for language specifications to separate universally valid axioms from implementation-dependent choices.
The paper explicitly identifies important limitations: its proof rules establish conditional, or partial, correctness rather than termination; they assume expressions and conditions have no side effects; and they do not yet cover features such as pointers, recursion, arrays, input/output, parallel execution, and complex parameter mechanisms. Hoare argues that these limitations should be made explicit in specifications and proofs rather than hidden in informal programming practice.
Influence
The system introduced in the paper became known as Hoare logic, or Floyd–Hoare logic, and its assertion triples and inference rules became a standard basis for deductive verification of imperative programs. Later accounts describe the precondition–program–postcondition triple, assignment rule, composition rule, and loop-invariant reasoning as core components of program logic. (doi.org)
The approach influenced subsequent work on programming-language semantics and verification, including axiomatic definitions of languages such as Pascal, automated program verification, and later extensions for concurrency, pointers, procedures, relational properties, and memory reasoning. Modern formal-methods texts and research continue to use Hoare-style reasoning as an entry point for verification-condition generation and proof-based software development. (sciencedirect.com)