Two theorems about the completeness of Hoare's logic

DOI10.1016/0020-0190(82)90095-3MaRDI QIDQ794426zbMATH OpenOpenAlexFDO

Authors John V. Tucker, J. A. Bergstra

Publication date 1982

Published in Information Processing Letters (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0020-0190(82)90095-3

zbMATH Keywords

proof theorycompletenessPeano arithmeticgenericityrefinementsdata type specificationsHoare's logicpartial correctness of while-programsstrongest post condition

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65)

Recommendations

• Expressiveness and the completeness of Hoare's logic
• Some general incompleteness results for partial correctness logics
• On relative completeness of Hoare logics
• Effective Axiomatizations of Hoare Logics
• scientific article; zbMATH DE number 3860376

Cites work

• scientific article; zbMATH DE number 3860376 (Why is no real title available?)
• scientific article; zbMATH DE number 3683036 (Why is no real title available?)
• scientific article; zbMATH DE number 3707731 (Why is no real title available?)
• scientific article; zbMATH DE number 3713172 (Why is no real title available?)
• scientific article; zbMATH DE number 3729430 (Why is no real title available?)
• scientific article; zbMATH DE number 3795350 (Why is no real title available?)
• scientific article; zbMATH DE number 3291134 (Why is no real title available?)
• An axiomatic basis for computer programming
• Floyd's principle, correctness theories and program equivalence
• Some natural structures which fail to possess a sound and decidable Hoare-like logic for their while-programs
• Soundness and Completeness of an Axiom System for Program Verification
• Ten Years of Hoare's Logic: A Survey—Part I
• Theory of program structures: Schemes, semantics, verification

Cited in

(32)

• On relative completeness of Hoare logics
• Effective Axiomatizations of Hoare Logics
• Inductive completeness of logics of programs
• A decomposition rule for the Hoare logic
• scientific article; zbMATH DE number 1512073 (Why is no real title available?)
• Some general incompleteness results for partial correctness logics
• Verification conditions are code
• scientific article; zbMATH DE number 3900131 (Why is no real title available?)
• scientific article; zbMATH DE number 3958718 (Why is no real title available?)
• scientific article; zbMATH DE number 90777 (Why is no real title available?)
• Expressiveness and the completeness of Hoare's logic
• Floyd-Hoare logic in iteration theories
• scientific article; zbMATH DE number 3888900 (Why is no real title available?)
• Average case optimality for linear problems
• Completeness of Hoare logic with inputs over the standard model
• scientific article; zbMATH DE number 3921949 (Why is no real title available?)
• A language independent proof of the soundness and completeness of generalized Hoare logic
• Relative completeness for logics of functional programs
• scientific article; zbMATH DE number 6845503 (Why is no real title available?)
• On the completeness of propositional Hoare logic
• scientific article; zbMATH DE number 3848601 (Why is no real title available?)
• Foundations of Software Science and Computation Structures
• scientific article; zbMATH DE number 3942998 (Why is no real title available?)
• Proving program inclusion using Hoare's logic
• scientific article; zbMATH DE number 3874578 (Why is no real title available?)
• scientific article; zbMATH DE number 3902002 (Why is no real title available?)
• Partial correctness: The term-wise approach
• The axiomatic semantics of programs based on Hoare's logic
• Hoare's logic and Peano's arithmetic
• The semantics of Hoare's iteration rule
• The \(\mathbf{M}\)-computations induced by accessibility relations in nonstandard models \(\mathbf{M}\) of Hoare logic
• Some questions about expressiveness and relative completeness in Hoare's logic

This page was built for publication: Two theorems about the completeness of Hoare's logic

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