Completeness of Hoare Logic Relative to the Standard Model

DOI10.1007/978-3-319-51963-0_10zbMATH Open1444.03122arXiv1703.00237OpenAlexW2571534558MaRDI QIDQ2971129FDOQ2971129

Wenhui Zhang, Zhaowei Xu, Yuefei Sui

Publication date: 4 April 2017

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

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.

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)

Cites Work

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

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)