Some questions about expressiveness and relative completeness in Hoare's logic
type: Item
instance of: scholarly article
title: Some questions about expressiveness and relative completeness in Hoare's logic
zbMATH Open document ID: 0575.68015
DOI: 10.1016/0304-3975(85)90138-0
published in: Theoretical Computer Science
publication date: 1985-01-01T00:00:00Z
review text: 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.
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 68N01
zbMATH DE Number: 3919786
zbMATH Keywords: Hoare's logic
zbMATH Keywords: while-programs
zbMATH Keywords: expressive structure
zbMATH Keywords: partial correctness assertion
author: M. Rodríguez Artalejo
MaRDI profile type: Publication
full work available at URL: 0304-3975(85)90138-0
OpenAlex ID: W2073711304
cites work: Q4198727
cites work: A complete logic for reasoning about programs via nonstandard model theory. II
cites work: Ten Years of Hoare's Logic: A Survey—Part I
cites work: Q4741695
cites work: Q3883473
cites work: Expressiveness and the completeness of Hoare's logic
cites work: Some natural structures which fail to possess a sound and decidable Hoare-like logic for their while-programs
cites work: Model theory
cites work: Soundness and Completeness of an Axiom System for Program Verification
cites work: Q4052071
cites work: An axiomatic basis for computer programming
cites work: Definability by programs in first-order structures
cites work: On the termination of program schemas
cites work: Q4766569
cites work: Q4164784
cites work: On the notion of expressiveness and the rule of adaptation
cites work: The unwind property in certain algebras
cites work: A New Incompleteness Result for Hoare's System
Recommended article: Expressiveness and the completeness of Hoare's logic
Recommended article: On relative completeness of Hoare logics
Recommended article: On the completeness of propositional Hoare logic
Recommended article: Q3765226
Recommended article: Q4501147
Recommended article: Two theorems about the completeness of Hoare's logic
Recommended article: Expressive power and incompleteness of propositional logics
Recommended article: Completeness and incompleteness for intuitionistic logic
Recommended article: A note on the complexity of propositional Hoare logic
Recommended article: Q4661992
description: scientific article; zbMATH DE number 3919786