An Axiomatic Basis for Computer Programming
đź“ś Abstract
The study of the logical foundations of computer programming is in a very early stage of development. The present paper is an attempt to explore the interesting and useful properties of the axiomatic method, first used by Euclid in his geometry, when applied to computer programming. Sets of axioms and rules of inference are given for a simple programming language; and examples of formal proofs of properties of programs are shown. The advantages and disadvantages of the approach are briefly discussed, and several illustrative examples are given.
✨ Summary
This paper, published in 1969 by C. A. R. Hoare, introduces an axiomatic approach to computer programming based on formal logic principles, akin to Euclidean geometry. Hoare proposes sets of axioms and inference rules for a simple programming language, allowing formal proofs of program properties. This work laid foundational principles for program verification and formal methods in computer science.
The paper was seminal in that it introduced what is now known as “Hoare Logic,” which remains a cornerstone in the fields of formal methods and software verification. The impact of this work is evidenced in its influence on numerous subsequent studies and methodologies related to formal methods and programming semantics. For example, Hoare’s axiomatic basis is instrumental in understanding program correctness and has influenced later languages and frameworks that aim to ensure or verify software correctness formally.
Hoare’s method was also a precursor to modern software verification tools, which are used extensively in critical systems where high reliability is necessary, such as in aerospace and medical software. The emphasis on proving program properties rigorously has further guided the development of various logic-based languages and frameworks that thrive in academic and industry settings.
References to this paper can be found in numerous later research articles, such as: - A comprehensive overview in A Survey of Formal Methods for Automated Software Analysis - Application of these principles in practical software systems as discussed in Formal Methods: State of the Art and Future Directions - A discussion on software verification in Software Verification and Validation: An Engineering and Scientific Approach
Hoare’s axiomatic basis laid the groundwork for the field of formal verification and program correctness, influencing both theoretical advancement and the practical application of these concepts in modern computer systems.