Two theorems about the completeness of Hoare's logic

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

Jan A. Bergstra, J. V. Tucker

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

completeness; data type specifications; proof theory; Peano arithmetic; genericity; refinements; Hoare's logic; partial correctness of while-programs; strongest post condition

Mathematics Subject Classification ID

68Q60: Specification and verification (program logics, model checking, etc.)

68Q65: Abstract data types; algebraic specification

Related Items

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

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