Precise Reasoning about Container-Internal Pointers with Logical Pinning

Yawen Guan

doi:10.1145/3779031.3779096

2026-01-01

PRE

Yawen Guan *

Clément Pit-Claudel

DOI：10.1145/3779031.3779096

原文链接

原文求助

摘要

En 中文

大多数分离逻辑隐藏了容器内部的指针以实现模块化。这使得难以指定临时将那些指针暴露给外部的容器API，以及验证使用这些API的程序。我们提出了一种逻辑固定（logical pinning）方法，这是一种轻量级的借用模型，用于顺序程序，允许用户在逻辑层面上选择性地跟踪容器内部的指针。我们的模型推广了魔法棒（magic-wand）算子以表示部分数据结构，使得编写和证明精确规范（包括指针稳定性属性）变得容易。由于它仅改变表示谓词和规范编写的方式，我们的方法与大多数分离逻辑变体兼容。我们通过验证小型但具有代表性的指针操作程序，并推导出常见容器规范更精确的版本，来展示逻辑固定的实用性。在此过程中，我们表明我们的方法涵盖了某些已知的证明模式，简化了某些复杂证明，并支持传统规范不支持的对程序模式的推理。所有结果都在Rocq证明助手中机械化实现，使用了CFML库。

Keyword:

Representation predicates

Containers

Sharing