Resource Morphisms for Specifying Concurrent Programs in Separation Logic
semanticscholar(2019)
摘要
In addition to preand postconditions, program specifications in recent separation logics for concurrency have employed an algebraic structure of resources—a form of state transition systems—to describe the state-based program invariants that must be preserved, and to record the permissible atomic changes to program state. In this paper we introduce a novel notion of resource morphism, i.e. structure-preserving function on resources, and show how to effectively integrate it into separation logic. We apply morphisms to abstract atomicity, where a program verified under one resource is adapted to operate under another resource, thus facilitating proof reuse.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要