Sciweavers

CSL
2002
Springer

Hoare Logics for Recursive Procedures and Unbounded Nondeterminism

13 years 11 months ago
Hoare Logics for Recursive Procedures and Unbounded Nondeterminism
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 have been checked with the theorem prover Isabelle/HOL.
Tobias Nipkow
Added 18 Dec 2010
Updated 18 Dec 2010
Type Journal
Year 2002
Where CSL
Authors Tobias Nipkow
Comments (0)