We formalize a Hoare logic for the partial correctness of while programs in PVS and prove its soundness and relative completeness. We use the PVS higher-order logic to define the syntax and semantics of a small imperative programming language, and describe a proof system for Hoare triples involving programs in this language. We prove the soundness of the proof system by demonstrating that only valid triples are provable. We also demonstrate the relative completeness of the proof system by defining the weakest liberal precondition operator and using it to prove that all valid Hoare triples are provable modulo the assertion logic. Finally, we verify a verification condition generator for Hoare logic Variants of Hoare logic have been formalized before in PVS and using other interactive proof assistants. We use Hoare logic as a tutorial exercise to illustrate the effective use of PVS in capturing the syntax and semantics of embedded logics. The embedding of Hoare logic is simple enough to be easily reproduced by the reader, but it also illustrates some of the nuances of formalization and proof using PVS, in particular, and higher-order logic, in general.
展开▼
