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.

• Type: Journal
• Year: 2002
• Where: CSL
• Authors: Tobias Nipkow
• Keywords: Automated Reasoning, CSL 2002, Procedures, Recursive Parameterless Procedures, Total Correctness