Parametric Completeness for Separation Theories
Parametric Completeness for Separation Theories
复制标题
DOI：
10.1145/2535838.2535844
复制
发表时间：
2014-01-01
影响因子：
--
通讯作者：
Villard, Jules
中科院分区：
文献类型：
--
作者：
Brotherston, James;Villard, Jules
在本文中，我们关闭的逻辑BBI，这是分离逻辑的命题基础，并在一个预期的类分离模型的有效性，如在分离逻辑的应用程序，如程序验证可证明性之间的逻辑差距。分离模型的预期类别通常由一组公理指定，这些公理描述了预期成立的特定模型属性，我们称之为分离理论。我们的主要贡献如下。首先，我们证明了分离理论的几个典型性质在BBI中是不可定义的。其次，我们表明，这些属性成为可定义的BBI在一个合适的混合扩展，通过添加一个理论的命名BBI以同样的方式，混合逻辑扩展正常模态逻辑。无绑定扩展HyBBI捕获了我们考虑的大多数属性，而带有混合逻辑常用的向下箭头绑定器的完整扩展HyBBI（向下箭头）涵盖了所有这些属性。第三，我们提出了一个公理证明系统，我们的混合逻辑的扩展与任何一组“纯”公理是健全的和完整的模型，满足这些公理。作为这个一般结果的推论，我们得到，在一个参数的方式，一个健全的和完整的公理证明系统，从我们考虑的类的任何分离理论。据我们所知，这门课包括了所有出现在出版文献中的分离理论。
In this paper, we close the logical gap between provability in the logic BBI, which is the propositional basis for separation logic, and validity in an intended class of separation models, as employed in applications of separation logic such as program verification. An intended class of separation models is usually specified by a collection of axioms describing the specific model properties that are expected to hold, which we call a separation theory. Our main contributions are as follows. First, we show that several typical properties of separation theories are not definable in BBI. Second, we show that these properties become definable in a suitable hybrid extension of BBI, obtained by adding a theory of naming to BBI in the same way that hybrid logic extends normal modal logic. The binder-free extension HyBBI captures most of the properties we consider, and the full extension HyBBI (down arrow) with the usual down arrow binder of hybrid logic covers all these properties. Third, we present an axiomatic proof system for our hybrid logic whose extension with any set of "pure" axioms is sound and complete with respect to the models satisfying those axioms. As a corollary of this general result, we obtain, in a parametric manner, a sound and complete axiomatic proof system for any separation theory from our considered class. To the best of our knowledge, this class includes all separation theories appearing in the published literature.