An axiomatic basis for computer programming

The work

AuthorsC. A. R. Hoare
Typearticle
Year1969
Citekeyhoare1969axiomatic

Where it appeared

Published inCommunications of the ACM
PublisherAssociation for Computing Machinery
Volume12
Issue10
Pages576--580

Identifiers

DOI10.1145/363235.363259
OpenAlexW2987907651

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.

A copy is held

pdf, 2.3 MB. Not published — it may be under copyright. The facts and links here are.

How it got here

How it got hereagent via openalex
Added2026-08-04 00:00 UTC
Approved bya person 2026-08-21 05:47 UTC

Cite it as

@article{hoare1969axiomatic,
  title        = {An axiomatic basis for computer programming},
  author       = {C. A. R. Hoare},
  year         = {1969},
  journal      = {Communications of the ACM},
  volume       = {12},
  number       = {10},
  pages        = {576--580},
  publisher    = {Association for Computing Machinery},
  doi          = {10.1145/363235.363259},
}

This record lives at https://refs.drheap.org/hoare1969axiomatic/ and will keep doing so.