Auxiliary Variables and Recursive Procedures
Auxiliary Variables and Recursive Procedures
复制标题
辅助变量和递归过程
DOI：
--
复制
发表时间：
1997
期刊：
影响因子：
--
通讯作者：
T. Schreiber
中科院分区：
文献类型：
--
作者：
T. Schreiber
公理语义学的许多研究都缺乏形式化。特别是，大多数针对处理递归过程的命令式程序提出的验证计算已知是不健全或不完整的。着眼于完全正确性，我们提出了一种新的结果规则，该规则在存在无参数递归过程的情况下产生健全且完整的霍尔式演算。标准结果和改进的适应规则都是我们新规则的实例。这项工作是在计算机辅助证明系统乐高的支持下开发的。对辅助变量的严格处理对于建立我们的结果至关重要。与 VDM 的比较强化了我们的观点，即辅助变量值得认真对待。
Much research in axiomatic semantics suffers from a lack of formality. In particular, most proposed verification calculi for imperative programs dealing with recursive procedures are known to be unsound or incomplete. Focussing on total correctness, we present a new consequence rule which yields a sound and complete Hoare-style calculus in the presence of parameterless recursive procedures. Both, the standard consequence and an improved rule of adaptation are instances of our new rule. This work has been developed under the auspices of the computer-aided proof system Lego. The rigorous treatment of auxiliary variables has been crucial for establishing our results. A comparison with VDM reinforces our view that auxiliary variables deserve to be treated seriously.