Hoare Logics for Recursive Procedures and Unbounded Nondeterminism
Hoare Logics for Recursive Procedures and Unbounded Nondeterminism
复制标题
递归过程和无界非确定性的霍尔逻辑
DOI：
--
复制
发表时间：
2002
期刊：
影响因子：
--
通讯作者：
T. Nipkow
中科院分区：
文献类型：
--
作者：
T. Nipkow
本文提出了健全的和完整的霍尔逻辑的部分和全部正确的递归无参数程序在无界不确定性的背景下。对于完全正确性，文献到目前为止要么限制递归过程是确定性的，要么只研究了与循环而不是过程结合的无界非确定性。我们考虑了单一的程序和系统的mutualrecursive程序。所有的证明都已经用定理证明器Isabelle/HOL进行了检查。
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 onlyi n conjunction with loops rather than procedures. We consider both single procedures and systems of mutuallyrecu rsive procedures. All proofs have been checked with the theorem prover Isabelle/HOL.