Hoare Logics in Isabelle/HOL

Tobias Nipkow

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.


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