Two theorems about the completeness of Hoare's logic
type: Item
instance of: scholarly article
title: Two theorems about the completeness of Hoare's logic
zbMATH Open document ID: 0541.68008
DOI: 10.1016/0020-0190(82)90095-3
author: John V. Tucker
author: J. A. Bergstra
published in: Information Processing Letters
publication date: 1982-01-01T00:00:00Z
review text: This paper continues a series of papers of these authors on Hoare's logic and its proof theory. The issue that is addressed here is the genericity of Hoare's logic among all possible logics for partial correctness of while-programs. The results of this paper indicate that, in some sense, Hoare's logic is generic. The main result is as follows. Let (\(\Sigma\),E) be some axiomatic specification, where \(\Sigma\) is a finite signature and E is a set of axiom written in \(L(\Sigma)\), the first-order language over \(\Sigma\). If this specification has only infinite models, then it can be extended to a specification \((\Sigma ',E'),\) i.e., \(\Sigma \subseteq \Sigma '\) and \(E\subseteq E',\) such that Hoare's logic is complete for partial correctness of while-programs over \((\Sigma ',E').\) Furthermore, this extension is conservative both for first-order assertions and partial correctness assertions. That is, if \(\phi\) is an assertion over \(\Sigma\), and \(\phi\) is true in all models of \((\Sigma ',E'),\) then \(\phi\) is true in all models of (\(\Sigma\),E).
Mathematics Subject Classification ID: 68Q65
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 03B15
zbMATH DE Number: 3860375
zbMATH Keywords: data type specifications
zbMATH Keywords: refinements
zbMATH Keywords: completeness
zbMATH Keywords: Peano arithmetic
zbMATH Keywords: strongest post condition
zbMATH Keywords: Hoare's logic
zbMATH Keywords: proof theory
zbMATH Keywords: genericity
zbMATH Keywords: partial correctness of while-programs
MaRDI profile type: Publication
full work available at URL: 0020-0190(82)90095-3
OpenAlex ID: W2019193580
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: Q3327706
cites work: Some natural structures which fail to possess a sound and decidable Hoare-like logic for their while-programs
cites work: Q3917477
cites work: Q3878740
cites work: Q4741695
cites work: Q3904041
cites work: Soundness and Completeness of an Axiom System for Program Verification
cites work: Theory of program structures: Schemes, semantics, verification
cites work: An axiomatic basis for computer programming
cites work: Q5573961
description: scientific article; zbMATH DE number 3860375