Effective axiomatizations of Hoare logics
The work
| Authors | Edmund M. Clarke Jr.; Steven M. German; Joseph Y. Halpern |
|---|---|
| Editors | |
| Type | article |
| Year | 1983 |
| Citekey | clarke1983effective |
Where it appeared
| Published in | Journal of the ACM |
|---|---|
| Volume | 30 |
| Issue | 3 |
| Pages | 612--636 |
Identifiers
| DOI | 10.1145/2402.322394 |
|---|
Abstract
For a wide class of programming languages P and expressive interpretations I, it is shown that there exist sound and relatively complete Hoare logics for both partial-correctness and termination assertions. In fact, under mild assumptions on P and I it is shown that the assertions true in I are uniformly decidable in the theory of I (Th(I)) iff the halting problem for P is decidable for finite interpretations. Moreover the set of true termination assertions is uniformly recursively enumerable in Th(I) even if the halting problem for P is not decidable for finite interpretations. Since total-correctness assertions coincide with termination assertions for deterministic programming languages, this last result unexpectedly suggests that good axiom systems for total correctness may exist for a wider spectrum of languages than is the case for partial correctness.
A copy is held
pdf, 1.3 MB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | agent via bibtex |
|---|---|
| Added | 2026-08-05 00:00 UTC |
| Approved by | a person 2026-08-16 15:32 UTC |
Cite it as
@article{clarke1983effective,
title = {Effective axiomatizations of Hoare logics},
author = {Edmund M. Clarke Jr. and Steven M. German and Joseph Y. Halpern},
year = {1983},
journal = {Journal of the ACM},
volume = {30},
number = {3},
pages = {612--636},
doi = {10.1145/2402.322394},
}
This record lives at https://refs.drheap.org/clarke1983effective/ and will keep doing so.