Two theorems about the completeness of Hoare's logic

DOI10.1016/0020-0190(82)90095-3zbMath0541.68008OpenAlexW2019193580MaRDI QIDQ794426

J. V. Tucker, Jan 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

completenessdata type specificationsproof theoryPeano arithmeticgenericityrefinementsHoare's logicpartial correctness of while-programsstrongest post condition

Mathematics Subject Classification ID

Related Items (5)

Some general incompleteness results for partial correctness logics ⋮ Hoare's logic and Peano's arithmetic ⋮ Proving program inclusion using Hoare's logic ⋮ Average case optimality for linear problems ⋮ The axiomatic semantics of programs based on Hoare's logic

Cites Work

• 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
• Theory of program structures: Schemes, semantics, verification
• Ten Years of Hoare's Logic: A Survey—Part I
• Soundness and Completeness of an Axiom System for Program Verification
• An axiomatic basis for computer programming
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

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