Expressiveness and the completeness of Hoare's logic

Citations of this article
Mendeley users who have this article in their library.


Three theorems are proven which reconsider the completeness of Hoare's logic for the partial correctness of while-programs equipped with a first-order assertion language. The results are about the expressiveness of the assertion language and the role of specifications in completeness concerns for the logic: (1) expressiveness is not a necessary condition on a structure for its Hoare logic to be complete, (2) complete number theory is the only extension of Peano Arithmetic which yields a logically complete Hoare logic and (3) a computable structure with enumeration is expressive if and only if its Hoare logic is complete. © 1982.




Bergstra, J. A., & Tucker, J. V. (1982). Expressiveness and the completeness of Hoare’s logic. Journal of Computer and System Sciences, 25(3), 267–284.

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free