买一送一：提升分离逻辑断言
Two for the Price of One: Lifting Separation Logic Assertions
摘要：
最近，数据抽象已经在分离逻辑的背景下进行了研究，并取得了显著的实际成功：开发的逻辑已经能够对棘手的挑战性程序进行清晰的证明，例如主体-观察者模式，并且它们已经成为Java（jStar），C（VeriFast）和Hoare类型论（Ynot）的有效验证工具的基础。在本文中，我们给出了一个新的语义分析，这种基于逻辑的方法，使用雷诺的关系参数。分析的核心是我们的提升定理，它给出了一个健全的和完整的条件，当一个真正的蕴涵之间的断言在标准的解释，需要相同的蕴涵保持在关系的解释。使用这些定理，我们提供了一个算法，用于识别抽象尊重客户端的证明，证明确保客户端不能区分两个适当相关的模块实现。
英文摘要：
Recently, data abstraction has been studied in the context of separation logic, with noticeable practical successes: the developed logics have enabled clean proofs of tricky challenging programs, such as subject-observer patterns, and they have become the basis of efficient verification tools for Java (jStar), C (VeriFast) and Hoare Type Theory (Ynot). In this paper, we give a new semantic analysis of such logic-based approaches using Reynolds's relational parametricity. The core of the analysis is our lifting theorems, which give a sound and complete condition for when a true implication between assertions in the standard interpretation entails that the same implication holds in a relational interpretation. Using these theorems, we provide an algorithm for identifying abstraction-respecting client-side proofs; the proofs ensure that clients cannot distinguish two appropriately-related module implementations.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
