#### Hoare Logics in Isabelle/HOL

This paper describes Hoare logics for a number of imperative
language constructs, from while-loops via exceptions to mutually
recursive procedures. Both partial and total correctness are
treated. In particular a proof system for total correctness of
recursive procedures in the presence of unbounded nondeterminism is
presented. All systems are formalized and shown to be sound and
complete in the theorem prover Isabelle/HOL.
pdf
ps

The Isabelle theories are available from the
Archive of Formal Proofs.

BibTeX:

@inproceedings{Nipkow-MOD2001,author={Tobias Nipkow},
title={Hoare Logics in {Isabelle/HOL}},
booktitle={Proof and System-Reliability},
editor={H. Schwichtenberg and R. Steinbr\"uggen},
publisher={Kluwer},year=2002,pages={341-367}}