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}