Effective Axiomatizations of Hoare Logics
Edmund M. Clarke, Steven M. German, Joseph Yehuda Halpern · Journal of the ACM · 1983
For a wtde class of programming languages P and expressive interpretations I, tt is shown that there exist sound and relauvely complete Hoare logics for both partiabcorrectness and termmatton assertions.In fact, under mild assumpUons on P and I it is shown that the assertions true in I are uniformly decidable in the theory of I (Th(I)) fit" the halting problem for P is decidable for fLmte interpretations.Moreover the set of true termination assertions is uniformly recursively enumerable m Th(1) even ff the halting problem for P ~s not dectdable 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 partml correctness.