Expressiveness and the completeness of Hoare's logic
type: Item
instance of: scholarly article
title: Expressiveness and the completeness of Hoare's logic
zbMATH Open document ID: 0549.68021
DOI: 10.1016/0022-0000(82)90013-7
author: John V. Tucker
author: J. A. Bergstra
published in: Journal of Computer and System Sciences
publication date: 1982-01-01T00:00:00Z
full work available at URL: https://dspace.library.uu.nl/handle/1874/13392
review text: The authors prove three theorems about completeness issues regarding Hoare's logic for while-programs: (1) expressiveness is not a necessary condition on a structure for the completeness of its Hoare logic, (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 iff its Hoare logic is complete. Here expressiveness means the ability of expressing strongest postconditions in first-order formulas over the structure concerned; a Hoare logic H is called complete relative to a structure A if any partial correctness formula valid over A is provable in H, where facts about A can be used as an oracle; a Hoare logic H is called logically complete with respect to a specification (theory) T if any partial correctness formula that is valid on all models of T is provable in H. The authors conclude from (1) that in general Cook's analysis of the completeness of Hoare logic is not sufficient, but also that by (3), in the most interesting cases in which computable structures are involved, Cook's notion of expressiveness is enough for the study of completeness. Since for every finite structure expressiveness is guaranteed, their Hoare logics are always complete. Moreover, for every infinite computable structure it is proved to be possible to enrich the signature, such that expressiveness becomes equivalent to completeness of the Hoare logic relative to the enriched structure. However, it is still an open problem whether this also holds in general for the original (infinite computable) structure. Finally a note on the use of Lemma 4.5 in the proof of Theorem 4.3 on p. 277: the three bottom lines have to be replaced by: ''From Lemma 4.5 and II(d) we obtain \(\vdash\neg \phi (x)\to\forall y(x\neq y)''.\)
Mathematics Subject Classification ID: 68Q65
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 03D60
Mathematics Subject Classification ID: 03C35
Mathematics Subject Classification ID: 03B60
zbMATH DE Number: 3876575
zbMATH Keywords: computable data structures
zbMATH Keywords: completeness
zbMATH Keywords: Hoare's logic for while- programs
zbMATH Keywords: expressiveness
zbMATH Keywords: complete number theory
zbMATH Keywords: computable structures
reviewed by: John-Jules Meyer
MaRDI profile type: Publication
OpenAlex ID: W1975577974
cites work: Ten Years of Hoare's Logic: A Survey—Part I
cites work: Q3899466
cites work: Floyd's principle, correctness theories and program equivalence
cites work: Some natural structures which fail to possess a sound and decidable Hoare-like logic for their while-programs
cites work: Q3904041
cites work: Q3904042
cites work: Hoare's logic for programming languages with two data types
cites work: Model theory
cites work: Programming Language Constructs for Which It Is Impossible To Obtain Good Hoare Axiom Systems
cites work: Corrigendum: Soundness and Completeness of an Axiom System for Program Verification
cites work: Theory of program structures: Schemes, semantics, verification
cites work: Specifying the Semantics of while Programs: A Tutorial and Critique of a Paper by Hoare and Lauer
cites work: An axiomatic basis for computer programming
cites work: Q3883459
cites work: CONSTRUCTIVE ALGEBRAS I
cites work: Q4160889
cites work: Computable Algebra, General Theory and Theory of Computable Fields
cites work: Q5537599
cites work: Q3050415
cites work: A New Incompleteness Result for Hoare's System
cites work: An axiomatic definition of the programming language Pascal
description: scientific article; zbMATH DE number 3876575