分离逻辑中的并行程序：态射与模拟
Specifying Concurrent Programs in Separation Logic: Morphisms and Simulations
摘要：
除了前置条件和后置条件，最近的并行分离逻辑中的程序规范采用了一种资源的代数结构-状态转换系统的一种形式-来描述必须保留的基于状态的程序不变量，并记录允许的程序状态原子变化。在本文中，我们引入了一个新的概念，资源态射，即资源上的结构保持功能，并展示了如何有效地将其集成到分离逻辑，使用相关的概念态射特定的模拟。我们将态射和模拟应用于在一种资源下验证的程序，以使它们在另一种资源下运行，从而促进证明重用。
英文摘要：
In addition to pre- and postconditions, program specifications in recent separation logics for concurrency have employed an algebraic structure of resources---a form of state transition system---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, using an associated notion of morphism-specific simulation. We apply morphisms and simulations to programs verified under one resource, to compositionally adapt them to operate under another resource, thus facilitating proof reuse.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
