Two theorems about the completeness of Hoare's logic (Q794426)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Two theorems about the completeness of Hoare's logic |
scientific article |
Statements
Two theorems about the completeness of Hoare's logic (English)
0 references
1982
0 references
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).
0 references
data type specifications
0 references
refinements
0 references
completeness
0 references
Peano arithmetic
0 references
strongest post condition
0 references
Hoare's logic
0 references
proof theory
0 references
genericity
0 references
partial correctness of while-programs
0 references
0 references