Relatively complete, and no better
A subject the papers are about. The loosest grouping, and the one to reach for last.
What Hoare logic can and cannot prove: complete only relative to an assertion language rich enough to state the invariants, and for some languages not even that.
The set is a single technical question pursued for seventy years, and it reads chronologically. Turing's 1949 *Checking a Large Routine* is the ancestor -- assertions attached to points in a program, in three pages, eighteen years before anyone took it up. Floyd in 1967 and Hoare in 1969 build the machinery; Hoare's 1971 paper on procedures introduces the feature that breaks it. Cook's soundness-and-completeness paper is the pivot, because the completeness it establishes is *relative* -- the logic is only as strong as the assertion language it draws on -- and everything after is an argument about what that concession costs.
The negative results are the set's spine and are why it is not merely a history. Clarke's 1976 and 1979 papers exhibit programming-language constructs for which no complete Hoare logic can exist at all; Lipton gives a necessary and sufficient condition; Bergstra and Tucker produce natural data structures that fail to possess a sound and complete axiomatisation. Expressiveness becomes the object of study in its own right -- Olderog, Grabowski, Artalejo, Kamin on stacks -- because after Cook that is where the difficulty was relocated.
Two extensions run alongside. Owicki and Gries in 1975-76 take it to parallel programs. Pointers and objects are the harder case: Bornat on proving pointer programs, Ishtiaq and O'Hearn's BI as an assertion language -- the paper separation logic grows out of -- and then the object-oriented sequence, beginning with De Boer's 1991 dissertation on a proof theory for concurrent object systems and running through Abadi and Leino, his own WP-calculus and Pierik to Apt's transformational account. That dissertation is the one record here taking both extensions at once.
Three records describe rival programmes rather than contributions to this one. Pratt's semantical considerations propose dynamic logic and Harel's *First-Order Dynamic Logic* develops it -- the set held the proposal without the development until 2026-08-31. Mirkowska and Salwicki's algorithmic logic is the Warsaw approach, reasoning about programs inside a logic rather than by a calculus over one. All three are held because a completeness question is what such a programme owes an account of.
Apt surveys it three times, in 1981, 1984 and 2019, and those are the fastest way in; Apt and Francez also supply the textbook treatments. Floyd 1967 appears twice, as the original and as the 1993 reprint in Colburn, Fetzer and Rankin, linked `reprint-of`. The corpus holds no copy of the Turing paper and every on-spec route to one has been tried and closed.