Two Theorems About the Completeness of Hoare's Logic

摘要

Two theorems about the completeness of Hoare's logic for the partial correctness of 'while' programs over an axiomatic specification are proven. The first result is a completion theorem: any specification (Sigma, E) can be refined to a specification (Sigma sub zero, E sub zero), conservative over (Sigma, E), whose Hoare's logic is complete. The second result is a normal form theorem: any complete specification (Sigma, E) possessing some complete logic for partial correctness can be refined to an effective specification (Sigma sub zero, E sub zero), conservative over (Sigma, E), which generates all true partial correctness formulas with Hoare's standard rules.