BI as an assertion language for mutable data structures
BI as an assertion language for mutable data structures
复制标题
DOI：
10.1145/373243.375719
复制
发表时间：
2001-03-01
影响因子：
--
通讯作者：
O'Hearn, PW
中科院分区：
文献类型：
--
作者：
Ishtiaq, S;O'Hearn, PW
雷诺兹开发了一种用于推理可变数据结构的逻辑，其中前置条件和后置条件以直观逻辑形式编写，并通过空间形式的连接来丰富。我们从 O'Hearn 和 Pym 的一堆含义的逻辑 BI 的角度研究了该方法。我们首先给出一个模型，其中排除中间定律成立，从而表明该方法与经典逻辑兼容。系统的直觉主义版本和经典版本之间的关系是通过翻译建立的，类似于从直觉逻辑到模态逻辑S4的翻译。我们还考虑公理的完整性问题。 BI 的空间蕴涵用于表达对象组件分配的最弱先决条件，并且在允许将命令应用于具有悬空指针的状态的三元组解释下，分配 cons 单元的公理被证明是完整的。我们通过合并操作和公理来处理内存，从而使后者成为一个功能。最后，我们描述了逻辑中的规范所享有的局部特征，并展示了如何自动推断出一类框架公理，即堆的哪些部分不会改变。
Reynolds has developed a logic for reasoning about mutable data structures in which the pre- and postconditions are written in an intuitionistic logic enriched with a spatial form of conjunction. We investigate the approach from the point of view of the logic BI of bunched implications of O'Hearn and Pym. We begin by giving a model in which the law of the excluded middle holds, thus showing that the approach is compatible with classical logic. The relationship between the intuitionistic and classical versions of the system is established by a translation, analogous to a translation from intuitionistic logic into the modal logic S4. We also consider the question of completeness of the axioms. BI's spatial implication is used to express weakest preconditions for object-component assignments, and an axiom for allocating a cons cell is shown to be complete under an interpretation of triples that allows a command to be applied to states with dangling pointers. We make this latter a feature, by incorporating an operation, and axiom, for disposing of memory. Finally, we describe a local character enjoyed by specifications in the logic, and show how this enables a class of frame axioms, which say what parts of the heap don't change, to be inferred automatically.