Hoare Logic and Auxiliary Variables
Hoare Logic and Auxiliary Variables
复制标题
霍尔逻辑和辅助变量
DOI：
10.1007/s001650050057
复制
发表时间：
1999
影响因子：
1
通讯作者：
["Thomas Kleymann
中科院分区：
文献类型：
--
作者：
["Thomas Kleymann
辅助变量对于在霍尔逻辑中指定程序是必不可少的。它们需要将不同状态下的变量值联系起来。然而，霍尔逻辑的公理和规则对辅助变量的作用视而不见。我们规定了一个新的结构规则，调整辅助变量时，加强先决条件和削弱后置条件。由于这一新规则，Hoare Logic是适应性完整的，这有利于软件的重用。这家酒店负责许多改进。相对完整性统一来自“最通用公式”属性。此外，可以表明霍尔逻辑包含维也纳开发方法（VDM）的操作分解规则，因为VDM中的每个推导可以自然地嵌入霍尔逻辑中。此外，新的治疗导致一个显着的简化演示验证演算处理更有趣的功能，如递归。
Auxiliary variables are essential for specifying programs in Hoare Logic. They are required to relate the value of variables in different states. However, the axioms and rules of Hoare Logic turn a blind eye to the role of auxiliary variables. We stipulate a new structural rule for adjusting auxiliary variables when strengthening preconditions and weakening postconditions. Courtesy of this new rule, Hoare Logic is adaptation complete, which benefits software re-use. This property is responsible for a number of improvements. Relative completeness follows uniformly from the Most General Formula property. Moreover, one can show that Hoare Logic subsumes Vienna Development Method's (VDM) operation decomposition rules in that every derivation in VDM can be naturally embedded in Hoare Logic. Furthermore, the new treatment leads to a significant simplification in the presentation for verification calculi dealing with more interesting features such as recursion.