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

Abstract

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 inexpressive- ness, relative incompleteness and strong relative incompleteness, and point out the seeming difficulty of answering them.