An Axiomatic Basis for Computer Programming
1969 · paper · Computer science
Explores the logical foundations of programming using axioms and rules of inference for proving properties of programs. It gives examples of such rules and a formal proof of a simple theorem. It argues that theoretical and practical advantages may follow.
Checked: PDF from cs.cmu.edu, fetched 4 Oct 2026. Page numbers are those of that PDF.
1 finding
Substance Section 2 (1) says that under the strict interpretation "the equalities of A1 to A9 are strict, in the sense that both sides exist or fail to exist together". In the paper's own strict model (Table II.1), A5 and A4 fail this when one factor is 0.
- p. 1 Section 2, item (1) Strict interpretation
the equalities of A1 to A9 are strict, in the sense that both sides exist or fail to exist together
- p. 2 Table II, 1. Strict Interpretation
* nonexistent
Only the authors can say what is right here.
Judge's note: I checked p.1 (the claim) and the Table II strict tables on p.2. Table II.1 gives 2+2 = *, 2×2 = * and 0×n = 0, and the strict interpretation is defined as 'the result of an overflowing operation does not exist; ... the offending program never completes its operation'. My own working: for A5 with x=0, y=z=2, the left side 0×(2+2) has to evaluate 2+2, which overflows, so it does not exist. The right side is 0×2+0×2 = 0+0 = 0, which exists. For A4, (0×2)×2 = 0 exists but 0×(2×2) does not. A1–A3 and A6–A9 do keep the property for nonnegative values, because intermediate sums never exceed the final sum. So the claim, as stated for all of A1–A9, is false in the paper's own model. Only the author can say whether to restrict the claim or the axioms.
Second check: another model agreed
Report a problem with this finding
3 minor (typos and the like; most checked by the judge only)
Typo In the key-word list, "theory of programming'" is followed by a raised apostrophe-like mark where a comma belongs.
- p. 1 KEY WORDS AND PHRASES
theory of programming'
Judge's note: The p.1 image shows a raised prime/apostrophe glyph after 'programming' at the end of the line. Every other key word is separated by a comma. This is a cosmetic print glitch.
Second check: none (judge only)
Report a problem with this finding
Typo In the proof of the second theorem in Section 2, the label 'A5' is set beside the starting expression "(r − y) + y × (1 + q)". The line A5 actually produces, "= (r − y) + (y × 1 + y × q)", has no label, while A9, A3 and A6 each label the line they produce.
- p. 1 Section 2, proof of second theorem
A5 (r − y) + y × (1 + q)
Judge's note: On the p.1 image, labels A9, A3 and A6 sit on the lines that result from applying them. A5 sits on line 1, and line 2 (the distributive step) is unlabelled. The labelling is therefore off by one line for A5. The proof itself is valid, so this is a cosmetic layout issue.
Second check: none (judge only)
Report a problem with this finding
Typo Reference 8 (Floyd, "Assigning meanings to programs. Proc. Amer. Math. Soc. Symposia in Applied Mathematics, Vol. 19, pp. 19-31.") gives no year, unlike the other entries.
- p. 6 References, item 8
Math. Soc. Symposia in Applied Mathematics, Vol. 19, pp. 19-31.
Only the authors can say what is right here.
Judge's note: Rests on outside knowledge: that the volume appeared in 1967 (I cannot check this from the files). The p.6 image confirms that entry 8 ends at 'pp. 19–31.' with no year, while references 1–7 and 9 all print one. The citation is incomplete but still identifiable. Both reviewer notes describe the same defect.
Second check: none (judge only)