链接数据结构中可达模式的逻辑
计算机科学中的逻辑
2007-06-13 v1
摘要
我们定义了一种新的可判定逻辑，用于表达和检查通过指针及破坏性指针更新操作动态分配对象的程序的不变量。该逻辑的主要特征是能够限制从指定节点通过正则表达式可达的节点邻域。该逻辑在布尔运算（蕴含、否定）下封闭，并具有有限模型性质。关键技术结果是可判定性的证明。我们展示了如何为一些有趣的程序表达前置条件、后置条件和循环不变量。此外，还可以表达诸如数据结构的不相交性以及底层堆突变等属性。而且，我们的逻辑可以表达任意数据结构的属性以及任意数量指针字段的属性。后者提供了一种自然的方法来指定后置条件，将过程入口处的字段与出口处的字段联系起来。因此，可以利用该逻辑自动证明执行底层堆突变的程序的部分正确性。
引用
@article{arxiv.0705.3610,
title = {A Logic of Reachable Patterns in Linked Data-Structures},
author = {Greta Yorsh and Alexander Rabinovich and Mooly Sagiv and Antoine Meyer and Ahmed Bouajjani},
journal= {arXiv preprint arXiv:0705.3610},
year = {2007}
}