首页    期刊浏览 2024年11月26日 星期二
登录注册

文章基本信息

  • 标题:Two for the Price of One: Lifting Separation Logic Assertions
  • 本地全文:下载
  • 作者:Jacob Thamsborg ; Lars Birkedal ; Hongseok Yang
  • 期刊名称:Logical Methods in Computer Science
  • 印刷版ISSN:1860-5974
  • 电子版ISSN:1860-5974
  • 出版年度:2012
  • 卷号:8
  • 期号:3
  • 页码:1
  • DOI:10.2168/LMCS-8(3:22)2012
  • 出版社:Technical University of Braunschweig
  • 摘要: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.
  • 其他关键词:separation logic, data abstraction, relational interpretation.
国家哲学社会科学文献中心版权所有