Local Reasoning about Programs that Alter Data Structures
Lecture Notes in Computer Science, 2001 · paper · Computer science
Extends Hoare logic to reason about programs that alter pointer-based data structures, using spatial conjunction and small axioms mentioning only the memory cells a command accesses. Examples show specifications and proofs can focus on those cells.
Checked: PDF from www0.cs.ucl.ac.uk, fetched 4 Oct 2026. Page numbers are those of that PDF.
4 findings
Substance p.13 property "j′ ≠ nil ∧ dl α (i, nil, j, j′) ⇒ ∃β, a, k. α ≐ βa ∗ dl β (i, i′, j′, k) ∗ j′ ↦ a, j − k" has a free i′ in the conclusion where nil is required.
- p. 13 first of the 'following properties'
dl β (i, i′, j′, k) ∗ j′ 7→a, j −k
Judge's note: My own working: the paper's end-of-list characterisation (p.13) is dl αa(i,i′,k,k′) ⇔ ∃j′. dl α(i,i′,k′,j′) ∗ k′ ↦ a, k−j′. Instantiating it with predecessor nil gives dl βa(i,nil,j,j′) ⇔ ∃k. dl β(i,nil,j′,k) ∗ j′ ↦ a, j−k. So the conclusion should read dl β(i,nil,j′,k). With i′ free the formula is false. Counterexample: take β=ε (a single element). The hypothesis forces the head field to be j−nil, while the conclusion forces it to be j−i′, so the implication fails whenever i′≠nil. The use in setrptr on p.14, dl α′(i,nil,j′,p), confirms that nil is meant.
Second check: another model agreed
Report a problem with this finding
Reference or label Reference [12] prints the page range "J. ACM, 47(1):267–223, January 2000." The start page is higher than the end page.
- p. 19 Reference [12]
J. ACM, 47(1):267–223, January 2000.
- p. 19 Reference [12]
47(1):267–223
Only the authors can say what is right here.
Judge's note: Both crops show "47(1):267–223" in the page image, so this is not an extraction artefact. A range that ends before it starts cannot be right. Reviewers suggest 167–223, but that rests on outside knowledge (the article's real first page), so the authors should confirm the correct start page.
Second check: another model agreed
Report a problem with this finding
Wording p.5 says "There is one axiom for each of four atomic commands", but the Small Axioms box lists five ([E]:=F, dispose(E), x:=cons(...), x:=E, x:=[E]).
- p. 5 Section 3, second paragraph
There is one axiom for each of four atomic commands.
- p. 5 The Small Axioms display
{E 7→–} dispose(E) {emp}
- p. 6 last paragraph
We have also included small axioms for the other two commands
Judge's note: On p.5 the box below the sentence shows five axioms. The next sentence names x:=E as an atomic command ('the only atomic command that can be described by Hoare's assignment axiom'). On p.6, after discussing the three heap commands, the text says 'small axioms for the other two commands', which also makes five. No definition in the paper reduces this to four. The axioms themselves are shown directly, so a reader is unlikely to be misled; I rate it as wording.
Second check: another model agreed
Report a problem with this finding
Wording The setlptr code on p.15 uses "[i + 1] := [i + 1] + i′ − k", nesting [·] inside an expression. This conflicts with p.5 ("[·] and cons do not appear within expressions") and with p.15 ("We could more simply write [j′+1] := k+[j′+1]−j if we were to allow nesting of [·]").
- p. 15 setlptr code, else branch
[i + 1] := [i + 1] + i′ −k
- p. 15 paragraph after setrptr
We could more simply write [j′ +1] := k +[j′ +1]−j if we were to allow nesting of [·].
- p. 5 Section 3
[·] and cons do not appear within expressions
Only the authors can say what is right here.
Judge's note: I checked the p.5 and p.15 images. setrptr uses a temporary variable d precisely to avoid nesting, and the text says nesting is not allowed. setlptr, a few lines later, nests [i+1] on the right-hand side, and the core system has no axiom for that form. The fix is probably a temporary variable, but only the authors can confirm it.
Second check: another model agreed
Report a problem with this finding
12 minor (typos and the like; most checked by the judge only)
Wording The p.15 prose describes the pre-dispose assertion as "(front ↦ a) ∗ (front + 1 ↦ n′ − nil) ∗ R", but the annotated assertion at that point is in terms of n ("front ↦ a, n − nil ∗ dl α (n, front, nil, back)"). The bound n′ is no longer in scope there.
- p. 15 paragraph after dequeue code
(front 7→a) ∗(front + 1 7→ n′ −nil) ∗R
- p. 15 dequeue annotation before dispose
{x .= a ∗front 7→a, n −nil ∗dl α (n, front, nil, back)}
Judge's note: In the p.15 dequeue annotations, n′ appears only in the second assertion. After n := d+nil the assertions use n. The prose's 'n′' is recoverable, since n equals n′ at that point, and the phrase 'of the form' leaves some latitude, so this is a minor consistency point.
Second check: another model agreed
Report a problem with this finding
Typo References [4] and [7] spell the author "S. Isthiaq", while the text (pp.1–2) spells it "Ishtiaq". A related slip is "Reearch Report 160" in ref [8].
- p. 18 Reference [4]
C. Calcagno, S. Isthiaq, and P. W. O’Hearn
- p. 18 Reference [7]
S. Isthiaq and P.W. O’Hearn
- p. 2 Introduction
by Ishtiaq and O’Hearn [7]
- p. 18 References, entries [4] and [7]
S. Isthiaq
Judge's note: The p.18 image shows 'Isthiaq' in [4] and [7]. The text layer has 'Ishtiaq' at lines 20, 65 and 67 (abstract and introduction). The p.19 image shows 'Report Reearch Report 160' in [8]. The other typos bundled into this cluster ('single-lement', 'is it similar') are handled in C005 and C002.
Second check: none (judge only)
Report a problem with this finding
Typo Grammar slips: p.9 "For x := [E] is it similar" (should be 'it is'); p.14 "putting an value a on the end of a queue" (should be 'a value').
- p. 9 weakest precondition paragraph
x := [E] is it similar
- p. 9 Section 4
For x := [E] is it similar
- p. 14 Section 7
putting an value a
- p. 14 before enqueue code
putting an value a on the end of a queue
Judge's note: Both phrases appear in the typeset text on the p.9 and p.14 page images. They are cosmetic.
Second check: none (judge only)
Report a problem with this finding
Typo p.9: "(where n ∉ Free(E, P, x)." opens a parenthesis that is never closed.
- p. 9 weakest precondition paragraph
(where n ̸∈Free(E, P, x).
- p. 9 weakest precondition for x := E
For x := [E] is it similar, using ∃to form a “let binder” (where n ̸∈Free(E, P, x).
Judge's note: The p.9 image shows only the closing parenthesis of Free(E,P,x) before the full stop. The parenthesis opened before 'where' is never closed.
Second check: none (judge only)
Report a problem with this finding
Typo The p.18 Conclusion has "the Shorr-Waite graph marking algorithm", while ref [23] on p.19 has "the Schorr-Waite graph marking algorithm".
- p. 18 Conclusion, first paragraph
the Shorr-Waite graph marking algorithm
- p. 19 Reference [23]
the Schorr-Waite graph marking algorithm
- p. 18 Conclusion, first paragraph
the Shorr-Waite graph
- p. 19 References, entry [23]
the Schorr-Waite
Judge's note: Both spellings are visible on the page images, so the paper is inconsistent with its own reference list. The 'is used' grammar slip is covered in C013, and the other typos listed here are covered in C002, C005 and C011.
Second check: none (judge only)
Report a problem with this finding
Typo p.13: "Thus, a single-lement list exemplifies" should read 'single-element'.
- p. 13 paragraph after the dl ab example
Thus, a single-lement list exemplifies
- p. 13 paragraph after dl a example
a single-lement list
- p. 13
Thus, a single-lement list exemplifies how
Judge's note: The misspelling appears in the typeset text on the p.13 image.
Second check: none (judge only)
Report a problem with this finding
Typo p.17: "The first, described in Section 8, to use a fault-avoiding interpretation" is missing 'is' (cf. 'The second is to use').
- p. 17 Conclusion, second paragraph
The first, described in Section 8, to use a fault-avoiding interpretation
Judge's note: The p.17 image shows the sentence without a verb. It is a cosmetic slip.
Second check: none (judge only)
Report a problem with this finding
Typo p.18: "Yang has treated a nontrivial example, the Shorr-Waite graph marking algorithm, using the spatial implication −∗ is used to deal with the sharing found there [23]" contains a stray 'is used' and does not parse.
- p. 18 Conclusion, first paragraph
using the spatial implication −∗is used to deal with the sharing found there [23]
- p. 18 Conclusion
using the spatial implication −∗is used to deal with the
Judge's note: The sentence on the p.18 image runs together two constructions. It is a cosmetic grammatical slip.
Second check: none (judge only)
Report a problem with this finding
Typo Ref [6]: "ECCOP’99 - Object-Oriented Programming, 13th European Conference" should read 'ECOOP’99'.
- p. 18 Reference [6]
ECCOP’99 - Object-Oriented Programming
- p. 18 refs [6],[1]
ECCOP’99
- p. 18 ref [1]
IEEE Transactions of Software Engineering
Only the authors can say what is right here.
Judge's note: Rests on outside knowledge: that the European Conference on Object-Oriented Programming is abbreviated ECOOP. The p.18 image shows 'ECCOP’99', and the acronym does not match the expanded title printed in the same entry. The 'Transactions of' point is handled in C015.
Second check: none (judge only)
Report a problem with this finding
Typo Ref [1]: "IEEE Transactions of Software Engineering" (the journal title is 'Transactions on').
- p. 18 References, entry [1]
IEEE Transactions of Software Engineering
Only the authors can say what is right here.
Judge's note: Rests on outside knowledge: that the journal is titled 'IEEE Transactions on Software Engineering'. The p.18 image shows 'Transactions of'. It is cosmetic.
Second check: none (judge only)
Report a problem with this finding
Typo Reference [8] misspells "Research": "Technical Report Reearch Report 160".
- p. 19 Reference [8]
Technical Report Reearch Report 160
- p. 19 ref [8]
Report Reearch Report 160
Judge's note: Checked in the page image: the entry reads "Technical Report Reearch Report 160, Compaq Systems Research Center". "Reearch" is a misspelling of "Research", and "Report ... Report" repeats a word.
Second check: none (judge only)
Report a problem with this finding
Typo Reference [11] gives a two-digit year, "5(2):215–244, June 99.", while every other entry uses four digits (e.g. "January 2000", "April 1999").
- p. 19 ref [11]
June 99
Judge's note: Checked in the page image: [11] ends "June 99.", and the other references give full years. This is a cosmetic style inconsistency only.
Second check: none (judge only)