Expressiveness and the completeness of Hoare's logic

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

Abstract

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.

Cite

CITATION STYLE

APA

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. https://doi.org/10.1016/0022-0000(82)90013-7

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