An Axiomatic Basis for Computer Programming.¶
Hoare, C. A. R. (1969). An Axiomatic Basis for Computer Programming. Communications of the ACM, 12(10), 576-580.
Cited by¶
8 citations across 8 artifacts.
Each citation links to the sentence it supports in the citing article.
Primes¶
- Algorithm
- The correctness-and-termination invariants (Hoare, 1969)
This sourceIntroduces Hoare logic with precondition/postcondition assertions as the formal framework for proving partial correctness (and, with termination, total correctness) of programs.
Supported in partVerified against the work's full text
Hoare gives pre/postcondition assertions and a loop invariant for conditional correctness, but explicitly says his axioms give no basis for proving termination.
“is that they give no basis for a proof that a program suc- cessfully terminates.”
- The correctness-and-termination invariants (Hoare, 1969)
- Ceteris Paribus
- And in legal and mathematical reasoning it is the scoped statement — "in cases where X holds, the rule provides Y" or "for any continuous function f" — in which the held-fixed condition is the hypothesis.
This sourceEstablishes precondition/postcondition reasoning, in which a program assertion is licensed only under its stated precondition — the held-fixed hypothesis under which a scoped (conditional) claim is provably correct, the formal analogue of a rule or theorem's hypothesis.
Supported in partVerified against the work's full text
Hoare shows a program claim P{Q}R holding only under a stated precondition, a formal analogue of a scoped conditional; it does not discuss legal rules or theorem hypotheses.
“This may be interpreted "If the assertion P is true before”
- And in legal and mathematical reasoning it is the scoped statement — "in cases where X holds, the rule provides Y" or "for any continuous function f" — in which the held-fixed condition is the hypothesis.
- Constraint
- … convex constraints and the duality between feasible sets and supporting hyperplanes; Montanari's 1974 formalization and Mackworth's 1977 arc-consistency algorithms founded constraint-satisfaction as a distinct computer-science subfield; Floyd's 1967 "Assigning Meanings to Programs" and Hoare's 1969 axiomatic semantics
This sourceFoundational paper introducing Hoare logic with pre/post-condition triples as the formal framework for proving partial correctness and termination invariants of algorithms.
- … convex constraints and the duality between feasible sets and supporting hyperplanes; Montanari's 1974 formalization and Mackworth's 1977 arc-consistency algorithms founded constraint-satisfaction as a distinct computer-science subfield; Floyd's 1967 "Assigning Meanings to Programs" and Hoare's 1969 axiomatic semantics
- Epistemic Mode Of A Proposition
- An
assert(x > 0)places the proposition "x > 0" in assert-mode: it must be checked, and the operation it licenses is "verify, and fail if false."This sourceIntroduces preconditions, postconditions, and loop invariants (Hoare logic), the formal apparatus distinguishing assertions checked from assumptions relied upon and invariants maintained.
Supported in partVerified against the work's full text
Hoare's iteration rule reasons that an assertion true on initiation and preserved by the loop body stays true after any number of iterations.
“Suppose P to be an assertion which is always true on completion of S, provided that it is also true on initiation. Then obviously P will still be true after any number of iterations of the statement S (even no iterations).”
- An
- Invariance
- … is the mechanism by which symmetries generate conservation laws (Noether's theorem gives the continuous-group version — each continuous symmetry of the action corresponds to a conserved quantity), topological invariants (genus, Euler characteristic, homotopy class) classify spaces up to deformation, loop invariants
This sourceFoundational paper introducing Hoare logic with pre/post-condition triples as the formal framework for proving partial correctness and termination invariants of algorithms.
- … is the mechanism by which symmetries generate conservation laws (Noether's theorem gives the continuous-group version — each continuous symmetry of the action corresponds to a conserved quantity), topological invariants (genus, Euler characteristic, homotopy class) classify spaces up to deformation, loop invariants
- Iteration
- The loop-invariant for correctness reasoning
This sourceFoundational paper introducing Hoare logic with pre/post-condition triples as the formal framework for proving partial correctness and termination invariants of algorithms.
SupportedVerified against the work's full text
Hoare's rule of iteration rests on an assertion preserved by every pass of the loop body, used to prove program properties such as the division example.
“Suppose P to be an assertion which is always true on completion of S, provided that it is also true on initiation. Then obviously P will still be true after any number of iterations of the statement S”
- The loop-invariant for correctness reasoning
Domain-specific¶
Verification¶
Does it exist? Confirmed. This work's DOI resolves to a registered record, which fixes its identity. That is all it fixes.
Does it back the claim? Read against the text for 4 of 8 citations: 1 supported, 3 supported in part. Each verdict is shown under its citation below, with what in the work backs the sentence.
Support is checked per citation rather than per work — the same source can be cited soundly in one article and wrongly in another. Per-citation recording began recently, so a citation with no recorded check is a gap in the record rather than evidence it went unchecked.
See how references were verified.
Registry ID ref:da4ab286cea9 · see in the full table