Hoare Logics for Recursive Procedures and Unbounded Nondeterminism

Tobias Nipkow

This paper presents sound and complete Hoare logics for partial and total correctness of recursive parameterless procedures in the context of unbounded nondeterminism. For total correctness, the literature so far has either restricted recursive procedures to be deterministic or has studied unbounded nondeterminism only in conjunction with loops rather than procedures. We consider both single procedures and systems of mutually recursive procedures. All proofs are performed with the help of the theorem prover Isabelle/HOL.

pdf ps

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

BibTeX:

@inproceedings{Nipkow-CSL02,author={Tobias Nipkow},
title={Hoare Logics for Recursive Procedures and Unbounded Nondeterminism},
booktitle={Computer Science Logic (CSL 2002)},editor={J. Bradfield},
publisher=Springer,series=LNCS,volume={2471},pages={103-119},year=2002}