一种非重复逻辑用于验证具有显式堆合取和析取的动态存储器
A Non-repetitive Logic for Verification of Dynamic Memory with Explicit Heap Conjunction and Disjunction
摘要：
在本文中，我们回顾了现有的点到分离逻辑的动态内存推理，我们发现，不同的使用堆分离往往是一个障碍。因此，两个总的和严格的空间堆操作堆图上提出，合取和析取-类似于逻辑合取。堆合取意味着存在一个可连接的空闲堆顶点，或者提供了一个显式的目标顶点。基本上，Burstall的性质不会改变。堆是指一个任意的简单有向图，它是有限的，可以包含代表类对象的复合顶点。限制任意堆内存访问，以及类型双关、后期类绑定和其他限制。新的逻辑的性质进行了调查，并作为一个结果组的属性。期望堆和表面堆都是可指定的。等价变换可能会使表示的堆不一致，尽管这些可以通过给出的两个通用线性规范化步骤检测和修补。这些属性有助于激励以后全面介绍堆上的一组等价物，以便将来工作。部分堆被认为是一种有用的规范技术，有助于减少规范的不完整性问题。最后，所提出的逻辑可以被考虑用于对象约束语言的扩展。
英文摘要：
In this paper, we review existing points-to Separation Logics for dynamic memory reasoning and we find that different usages of heap separation tend to be an obstacle. Hence, two total and strict spatial heap operations are proposed upon heap graphs, for conjunction and disjunction -- similar to logical conjuncts. Heap conjunction implies that there exists a free heap vertex to connect to or an explicit destination vertex is provided. Essentially, Burstall's properties do not change. By heap we refer to an arbitrary simple directed graph, which is finite and may contain composite vertices representing class objects. Arbitrary heap memory access is restricted, as well as type punning, late class binding and further restrictions. Properties of the new logic are investigated, and as a result group properties are shown. Both expecting and superficial heaps are specifiable. Equivalence transformations may make denotated heaps inconsistent, although those may be detected and patched by the two generic linear canonization steps presented. The properties help to motivate a later full introduction of a set of equivalences over heap for future work. Partial heaps are considered as a useful specification technique that help to reduce incompleteness issues with specifications. Finally, the logic proposed may be considered for extension for the Object Constraint Language.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
