Completeness of Hoare logic relative to the standard model

DOI10.1007/978-3-319-51963-0_10MaRDI QIDQ2971129zbMATH OpenOpenAlexFDO

Authors Zhaowei Xu, Wenhui Zhang, Yuefei Sui

Publication date 4 April 2017

Published in SOFSEM 2017: Theory and Practice of Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1703.00237

zbMATH Keywords

Peano arithmeticstandard modelHoare logicarithmetical hierarchyrelative completeness

Mathematics Subject Classification ID

Logic in computer science (03B70) First-order arithmetic and fragments (03F30) Models of arithmetic and set theory (03C62)

Abstract: The general completeness problem of Hoare logic relative to the standard model $N$ of Peano arithmetic has been studied by Cook, and it allows for the use of arbitrary arithmetical formulas as assertions. In practice, the assertions would be simple arithmetical formulas, e.g. of a low level in the arithmetical hierarchy. In addition, we find that, by restricting inputs to $N$, the complexity of the minimal assertion theory for the completeness of Hoare logic to hold can be reduced. This paper further studies the completeness of Hoare Logic relative to $N$ by restricting assertions to subclasses of arithmetical formulas (and by restricting inputs to $N$). Our completeness results refine Cook's result by reducing the complexity of the assertion theory.

Recommendations

• Completeness of Hoare logic with inputs over the standard model
• On relative completeness of Hoare logics
• Expressiveness and the completeness of Hoare's logic
• scientific article; zbMATH DE number 3860376
• On the completeness of propositional Hoare logic

Cites work

• scientific article; zbMATH DE number 4057487 (Why is no real title available?)
• scientific article; zbMATH DE number 4091484 (Why is no real title available?)
• scientific article; zbMATH DE number 51556 (Why is no real title available?)
• scientific article; zbMATH DE number 1556014 (Why is no real title available?)
• scientific article; zbMATH DE number 2110621 (Why is no real title available?)
• An axiomatic basis for computer programming
• Completeness of Hoare logic with inputs over the standard model
• Computability and Logic
• Effective Axiomatizations of Hoare Logics
• Expressiveness and the completeness of Hoare's logic
• Hoare logic and auxiliary variables
• Hoare's logic and Peano's arithmetic
• On relative completeness of Hoare logics
• On the completeness of propositional Hoare logic
• Programming Language Constructs for Which It Is Impossible To Obtain Good Hoare Axiom Systems
• Recursive assertions are not enough - or are they?
• Soundness and Completeness of an Axiom System for Program Verification
• Ten Years of Hoare's Logic: A Survey—Part I
• Ten years of Hoare's logic: A survey. II: Nondeterminism

Cited in

(5)

• scientific article; zbMATH DE number 1512073 (Why is no real title available?)
• Completeness of Hoare logic with inputs over the standard model
• Weak arithmetic completeness of object-oriented first-order assertion networks
• The \(\mathbf{M}\)-computations induced by accessibility relations in nonstandard models \(\mathbf{M}\) of Hoare logic
• Arithmetical completeness versus relative completeness

This page was built for publication: Completeness of Hoare logic relative to the standard model

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2971129)