一举两得：提升分离逻辑断言
编程语言
2015-07-01 v2
摘要
近期，数据抽象在分离逻辑的背景下得到了研究，并取得了显著的实践成功：所开发的逻辑使得诸如主题 - 观察者模式等棘手挑战性程序的简洁证明成为可能，并成为 Java (jStar)、C (VeriFast) 和 Hoare 类型理论 (Ynot) 高效验证工具的基础。在本文中，我们利用 Reynolds 的关系参数性，对此类基于逻辑的方法给出了新的语义分析。分析的核心是我们的提升定理，该定理给出了一个可靠且完备的条件，用于判断标准解释中断言间的真实蕴含关系是否意味着同样的蕴含关系在关系解释中也成立。利用这些定理，我们提供了一种算法来识别尊重抽象的客户端证明；这些证明确保客户端无法区分两个适当相关的模块实现。
引用
@article{arxiv.1208.5895,
title = {Two for the Price of One: Lifting Separation Logic Assertions},
author = {Jacob Thamsborg and Lars Birkedal and Hongseok Yang},
journal= {arXiv preprint arXiv:1208.5895},
year = {2015}
}