The Underlying Logic of Hoare Logic

Formulas of Hoare logic are asserted programs where is a program and , are assertions. The language of programs varies; in the survey [Apt 1980], one finds the language of while programs and various extensions of it. But the assertions are traditionally expressed in first-order logic (or extensions of it). In that sense, first-order logic is the underlying logic of Hoare logic. We question the tradition and demonstrate, on the simple example of while programs, that alternative assertion logics have some advantages. For some natural assertion logics, the expressivity hypothesis in Cook's completeness theorem is automatically satisfied. The readers of this column know Quisani, an inquisitive former student of one of us. This conversation is somewhat different because Quisani talks to both of the authors at once. Taking into account the magnitudes of our literary talents, we simplified the record of the conversation by blending the two authors into one who prefers "we"...

• Type: Journal
• Year: 2000
• Where: EATCS
• Authors: Andreas Blass, Yuri Gurevich
• Keywords: Assertion Logics, EATCS 2000, Hoare Logic, Logics