基于sheafeology的通用资源分离逻辑

分离逻辑最初是为了使指针程序的验证能够扩展到大型系统，已被证明极其有效。其核心思想是程序通常仅访问内存的局部部分，从而实现局部推理。这种方法通过将一阶逻辑扩展带有分离联合子来实现，后者检查内存的局部区域。事实上，这种方法不仅适用于指针程序，也适用于涉及其他资源结构的程序。已提出多种理论以提取并更广泛地应用分离逻辑的思想。这导致对内存的代数抽象以及针对并发程序和随机过程的各种分离逻辑变体。然而，现有方法中没有一种能够立即为不同资源的程序逻辑提供的一阶逻辑与分离联合子的组合形式。在本文中，我们提出一种基于分离逻辑可被资源化的一阶逻辑框架的方案。一阶逻辑可通过范畴逻辑（具体为纤维）来理解。我们的贡献在于通过在小束范畴中内部开发范畴逻辑，使其资源化，我们称之为sheafeology。小束的作用是通过资源的视图来建模资源，从而实现资源的局部分辨和组合，实现分离逻辑所承诺的可扩展性。我们提供了在小束范畴中构建内部纤维的构造方法，用于建模资源上的谓词，并且容许一阶联合子和分离联合子。由此，我们实现了通用资源的分离逻辑框架，并通过对多种内存模型和随机变量的实例化来支撑该框架。