Hoare's Logic and Peano's Arithmetic

摘要

A proof of Hoare's logic for the partial correctness of while-programs applied to arithmetic as defined by Pano's axioms is developed. The verification of programs in N arithmetic is considered without the privilege of N being on outright given structure and with the restriction that N must be axiomatically defined. The verification of an entirely proof-theoretic basis in Hoare's logic is studied. Proofs are given on what can be derived from arithmetic and on what can be stated about N in a specification. A representation of the strongest postcondition calculus in Peano arithmetic PA enables Hoare's logic over PA to be shown to be equivalent to PA itself.