Hoare's logic and Peano's arithmetic

DOI10.1016/0304-3975(83)90107-XzbMath0497.68007MaRDI QIDQ1170877

J. V. Tucker, Jan A. Bergstra

Publication date: 1983

Published in: Theoretical Computer Science (Search for Journal in Brave)

zbMATH Keywords

partial correctness of while-programs

Mathematics Subject Classification ID

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

Related Items (6)

Completeness of Hoare logic with inputs over the standard model ⋮ Completeness of Hoare Logic Relative to the Standard Model ⋮ Reasoning in Dynamic Logic about Program Termination ⋮ 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

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Two theorems about the completeness of Hoare's logic
• 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
• Automatic program verification. I: A logical basis and its implementation
• Abstract Data Type Specification in the Affirm System
• Verification of Array, Record, and Pointer Operations in Pascal
• 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

This page was built for publication: Hoare's logic and Peano's arithmetic