Some questions about expressiveness and relative completeness in Hoare's logic (Q1064046)

A well-known result of Cook asserts the completeness of Hoare's logic for while-programs relative to any expressive structure. In this paper we present a wide and natural class of structures whose members are either expressive or make Hoare's logic strongly incomplete relative to them, in the sense that a trivially true partial correctness assertion is not Hoare-derivable from the first order theory of the structure. The definition of this class is related to the so-called unwind property for while-programs, and its behaviour follows from quite general sufficient conditions for strong relative incompleteness. We state also two questions about the connections among inexpressiveness, relative incompleteness and strong relative incompleteness, and point out the seeming difficulty of answering them.