Two theorems about the completeness of Hoare's logic |
| |
| Authors: | J.A. Bergstra J.V. Tucker |
| |
| Affiliation: | Department of Computer Science, University of Leiden, 2300 RA Leiden, The Netherlands;Department of Computer Studies, University of Leeds, Leeds, LS2 9JT, Great Britain |
| |
| Abstract: | We prove two theorems about the completeness of Hoare's logic for the partial correctness of while-programs over an axiomatic specification. The first result is a completion theorem: any specification (Σ,E) can be refined to a specification (Σ0, E0), conservative over (Σ, E), whose Hoare's logic is complete. The second result is a normal form theorem: any complete specification (Σ, E) possessing some complete logic for partial correctness can be refined to an effective specification (Σ0, E0) conservative over (Σ, E), which generates all true partial correctness formulae with Hoare's standard rules. |
| |
| Keywords: | Hoare's logic partial correctness data type specifications refinements strongest postcondition calculus Peano arithmetic logical completeness |
| 本文献已被 ScienceDirect 等数据库收录！ |
|
