The Relationship between Separation Logic and Implicit Dynamic Frames
The Relationship between Separation Logic and Implicit Dynamic Frames
复制标题
分离逻辑与隐式动态框架的关系
DOI：
10.2168/lmcs-8(3:1)2012
复制
发表时间：
2011
影响因子：
8.7
通讯作者：
Alexander J. Summers
中科院分区：
文献类型：
--
作者：
Matthew J. Parkinson;Alexander J. Summers
分离逻辑是一种简洁的方法，用于指定操作动态分配存储的程序。部分灵感来自分离逻辑，隐式动态框架最近被提出，旨在一阶工具支持。在本文中，我们提供了一个标准的分离逻辑的全堆语义，并证明它等价于标准模型。通过小的调整，我们展示了如何给隐式动态框架一个直接的语义，并显示这种语义正确地捕捉现有的定义。这正好把两个逻辑联系起来。作为这种连接的结果，我们表明，一个片段的分离逻辑可以忠实地编码在一阶自动验证工具（圣杯）。
Separation logic is a concise method for specifying programs that manipulate dynamically allocated storage. Partially inspired by separation logic, Implicit Dynamic Frames has recently been proposed, aiming at first-order tool support. In this paper, we provide a total heap semantics for a standard separation logic, and prove it equivalent to the standard model. With small adaptations, we then show how to give a direct semantics to implicit dynamic frames and show this semantics correctly captures the existing definitions. This precisely connects the two logics. As a consequence of this connection, we show that a fragment of separation logic can be faithfully encoded in a first-order automatic verification tool (Chalice).
DOI：
10.1145/964001.964024
发表时间：
2004-01
期刊：
Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages
影响因子：
--
作者：
P. O'Hearn;Hongseok Yang;J. C. Reynolds
通讯作者：
P. O'Hearn;Hongseok Yang;J. C. Reynolds