一种用于带有显式堆合取与析取动态内存验证的非重复逻辑

在本文中，我们回顾了现有的用于动态内存推理的指向分离逻辑，发现堆分离的不同用法往往构成障碍。因此，基于堆图提出了两种用于合取与析取的总的严格空间堆操作——类似于逻辑合取。堆合取意味着存在一个空闲堆顶点可连接，或提供了显式目标顶点。本质上，Burstall 的性质不变。所谓堆是指任意有限简单有向图，可包含表示类对象的复合顶点。任意堆内存访问受到限制，类型双关、晚期类绑定等进一步受限。研究了新逻辑的性质，并由此展示了组性质。期望堆与表面堆均可规约。等价变换可能使指称堆不一致，尽管这些可由所提出的两个通用线性规范化步骤检测并修补。这些性质有助于激励未来工作中随后完整引入一组堆上的等价关系。部分堆被视为一种有用的规约技术，有助于减少规约的不完备性问题。最后，所提逻辑可考虑扩展至对象约束语言（Object Constraint Language）。