Two theorems about the completeness of Hoare's logic

DOI10.1016/0020-0190(82)90095-3zbMATH Open0541.68008OpenAlexW2019193580MaRDI QIDQ794426FDOQ794426

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

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

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)

Cites Work

• 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
• Title not available (Why is that?)
• Theory of program structures: Schemes, semantics, verification
• Floyd's principle, correctness theories and program equivalence
• Title not available (Why is that?)
• Some natural structures which fail to possess a sound and decidable Hoare-like logic for their while-programs
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)

Cited In (32)

• Inductive completeness of logics of programs
• A decomposition rule for the Hoare logic
• Title not available (Why is that?)
• Some general incompleteness results for partial correctness logics
• Title not available (Why is that?)
• Title not available (Why is that?)
• Verification conditions are code
• Title not available (Why is that?)
• Expressiveness and the completeness of Hoare's logic
• Floyd-Hoare logic in iteration theories
• Title not available (Why is that?)
• Average case optimality for linear problems
• Completeness of Hoare logic with inputs over the standard model
• Title not available (Why is that?)
• Relative completeness for logics of functional programs
• A language independent proof of the soundness and completeness of generalized Hoare logic
• Title not available (Why is that?)
• Title not available (Why is that?)
• On the completeness of propositional Hoare logic
• Foundations of Software Science and Computation Structures
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Proving program inclusion using Hoare's logic
• 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
• On relative completeness of Hoare logics
• Effective Axiomatizations of Hoare Logics

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)